# HG changeset patch
# User wenzelm
# Date 1472758126 -7200
# Node ID 0f61ea70d3843932aa8fe3d044bb20fbad99dfa9
# Parent  6920b1885eff24a1d551b4589afa8b8bee6c7562
clarified session: use all theories in directory HOL/Library;

diff -r 6920b1885eff -r 0f61ea70d384 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