Delete trailing whitespace in src/

conjecturing + parallel translate

Promote more Isabelle concurrency code

Portable gets slightly richer with

make_counter : {inc:int,init:int} -> unit -> int
syncref : 'a -> {get:unit->'a, upd : ('a -> 'b * 'a) -> 'b}

Under Moscow ML these map to obvious operations on references. Under
Poly/ML these map to synchronised variables that are operated on
atomically.

conjecturing: using gnu parallel instead of parmap

conjecturing: integration of eprover calls

holyhammer: parallelizable eprover calls

share code between tacticToe and holyHammer + start exp with conjecturing

holyhammer: finalizing port of the translation to SML + adding vampire

holyhammer: evaluation of old and new hammer

holyhammer: fixing unsoundness bug due to different names for the same variable

holyhammer: log functions

holyhammer: finishing porting the translation to sml (hh_new function)

tactictoe: adding create_fof function + improve parallelism

tactictoe: fix many issues in eprover_eval: missing theorems + update_hh_stac + atp problems + eprover_save_flag + omit tactictoe recording

remove trailing white spaces

tactictoe: interactive recording + examples + readme

holyhammer: fix error by matching the changes in hhsPredict

minimization and prettification shared between tactictoe and holyhammer

removing external predictors

tactictoe: reverting back the right print_vartype for first order

tactictoe: monte carlo wip

holyhammer: exporting theories by adding a filter on write_thyl

holyhammer signature

tactictoe: online recording (to be fixed)

tactictoe: interactive recording function

holyhammer: tactic + pretty-printing

Fix some infelicities in holyhammer build details

Trying to build with Moscow ML revealed a dependency on code in
tactictoe, so I reordered the directories in the build sequence. But
then, tactictoe is only built under Poly/ML anyway. So, I added the
[poly] annotation to the holyhammer directories too.

Changing the order may then seem unnecessary, but if one was to try to
exercise any of the holyhammer code, as part of a regression test for
example, then the tactictoe code does need to have been processed and
put in sigobj for that to work.

tactictoe: theorems' features IO + orthogonalization of theorems

holyhammer: removing scripts + tactictoe: wip+ sharing predictors

holyhammer: updating hh_try function

holyHammer update: provers' binaries now needs to be in PATH + working toward incremental export

holyhammer 1.0