# HG changeset patch
# User haftmann
# Date 1481984533 -3600
# Node ID 293ab573d03484d786bec68d75b2e175ed056a4a
# Parent  8355a6e2df79a562656ceebafaff04e429f88554
clarified library contents

diff -r 8355a6e2df79 -r 293ab573d034 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Library/Library.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -49,12 +49,14 @@
   More_List
   Multiset_Order
   Multiset_Permutations
+  Nonpos_Ints
   Numeral_Type
   Omega_Words_Fun
   OptionalSugar
   Option_ord
   Order_Continuity
   Parallel
+  Periodic_Fun
   Perm
   Permutation
   Permutations
@@ -72,6 +74,7 @@
   Quotient_Type
   Ramsey
   Reflection
+  Rewrite
   Saturated
   Set_Algebras
   State_Monad
diff -r 8355a6e2df79 -r 293ab573d034 src/HOL/ROOT
--- a/src/HOL/ROOT	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/ROOT	Sat Dec 17 15:22:13 2016 +0100
@@ -31,18 +31,14 @@
   *}
   theories
     Library
-    Nonpos_Ints
-    Periodic_Fun
     Polynomial_Factorial
-    Predicate_Compile_Quickcheck
+    (*conflicting type class instantiations and dependent applications*)
+    Finite_Lattice
+    List_lexord
     Prefix_Order
-    Rewrite
-    (*conflicting type class instantiations*)
-    List_lexord
-    Sublist_Order
     Product_Lexorder
     Product_Order
-    Finite_Lattice
+    Sublist_Order
     (*data refinements and dependent applications*)
     AList_Mapping
     Code_Binary_Nat
@@ -54,11 +50,13 @@
     DAList_Multiset
     RBT_Mapping
     RBT_Set
+    (*prototypic tools*)
+    Predicate_Compile_Quickcheck
     (*legacy tools*)
-    Refute
     Old_Datatype
     Old_Recdef
     Old_SMT
+    Refute
   document_files "root.bib" "root.tex"
 
 session "HOL-Hahn_Banach" in Hahn_Banach = HOL +