clarified session: use all theories in directory HOL/Library;
authorwenzelm
Thu, 01 Sep 2016 21:28:46 +0200
changeset 63763 0f61ea70d384
parent 63762 6920b1885eff
child 63764 f3ad26c4b2d9
clarified session: use all theories in directory HOL/Library;
src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Sep 01 20:59:51 2016 +0200
+++ b/src/HOL/ROOT	Thu Sep 01 21:28:46 2016 +0200
@@ -31,8 +31,12 @@
   *}
   theories
     Library
+    Nonpos_Ints
+    Periodic_Fun
+    Polynomial_Factorial
+    Predicate_Compile_Quickcheck
+    Prefix_Order
     Rewrite
-    Nonpos_Ints
     (*conflicting type class instantiations*)
     List_lexord
     Sublist_Order