Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
discontinued futile attempt to hardwire build options into the image, sequential mode is enabled more robustly at runtime (cf. 3b0a60eee56e);
authorwenzelm
Mon, 24 Sep 2012 16:13:56 +0200
changeset 505650a82e98fd4a3
parent 50564 3b0a60eee56e
child 50566 9b12fcd0a889
discontinued futile attempt to hardwire build options into the image, sequential mode is enabled more robustly at runtime (cf. 3b0a60eee56e);
src/HOL/Mirabelle/Mirabelle.thy file | annotate | diff | comparison | revisions 
     1.1 --- a/src/HOL/Mirabelle/Mirabelle.thy	Mon Sep 24 15:37:58 2012 +0200
     1.2 +++ b/src/HOL/Mirabelle/Mirabelle.thy	Mon Sep 24 16:13:56 2012 +0200
     1.3 @@ -9,10 +9,6 @@
     1.4  ML_file "Tools/mirabelle.ML"
     1.5  ML_file "../TPTP/sledgehammer_tactics.ML"
     1.6  
     1.7 -(* no multithreading, no parallel proofs *)  (* FIXME *)
     1.8 -ML {* Multithreading.max_threads := 1 *}
     1.9 -ML {* Goal.parallel_proofs := 0 *}
    1.10 -
    1.11  ML {* Toplevel.add_hook Mirabelle.step_hook *}
    1.12  
    1.13  ML {*
wneuper/isa