eliminated obsolete "parallel_proofs = 0" restriction (cf. 0e5b859e1c91)
authortraytel
Tue, 04 Sep 2012 12:12:03 +0200
changeset 49110 2e43fb45b91b
parent 49109 0e5b859e1c91
child 49111 9d511132394e
eliminated obsolete "parallel_proofs = 0" restriction (cf. 0e5b859e1c91)
src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Sep 04 12:10:19 2012 +0200
+++ b/src/HOL/ROOT	Tue Sep 04 12:12:03 2012 +0200
@@ -624,13 +624,10 @@
     Lambda_Term
     Process
     TreeFsetI
-  (* FIXME: shouldn't require "parallel_proofs = 0";
-     with parallel proofs enabled, the build of this session takes 10 times longer *)
-  theories [parallel_proofs = 0]
     "Infinite_Derivation_Trees/Gram_Lang"
     "Infinite_Derivation_Trees/Parallel"
     Stream
-  theories [parallel_proofs = 0, condition = ISABELLE_FULL_TEST]
+  theories [condition = ISABELLE_FULL_TEST]
     Misc_Codata
     Misc_Data