clarified library contents
authorhaftmann
Sat Dec 17 15:22:13 2016 +0100 (2016-12-17)
changeset 64588293ab573d034
parent 64587 8355a6e2df79
child 64589 c1932a4a227f
clarified library contents
src/HOL/Library/Library.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/Library/Library.thy	Sat Dec 17 15:22:13 2016 +0100
     1.2 +++ b/src/HOL/Library/Library.thy	Sat Dec 17 15:22:13 2016 +0100
     1.3 @@ -49,12 +49,14 @@
     1.4    More_List
     1.5    Multiset_Order
     1.6    Multiset_Permutations
     1.7 +  Nonpos_Ints
     1.8    Numeral_Type
     1.9    Omega_Words_Fun
    1.10    OptionalSugar
    1.11    Option_ord
    1.12    Order_Continuity
    1.13    Parallel
    1.14 +  Periodic_Fun
    1.15    Perm
    1.16    Permutation
    1.17    Permutations
    1.18 @@ -72,6 +74,7 @@
    1.19    Quotient_Type
    1.20    Ramsey
    1.21    Reflection
    1.22 +  Rewrite
    1.23    Saturated
    1.24    Set_Algebras
    1.25    State_Monad
     2.1 --- a/src/HOL/ROOT	Sat Dec 17 15:22:13 2016 +0100
     2.2 +++ b/src/HOL/ROOT	Sat Dec 17 15:22:13 2016 +0100
     2.3 @@ -31,18 +31,14 @@
     2.4    *}
     2.5    theories
     2.6      Library
     2.7 -    Nonpos_Ints
     2.8 -    Periodic_Fun
     2.9      Polynomial_Factorial
    2.10 -    Predicate_Compile_Quickcheck
    2.11 +    (*conflicting type class instantiations and dependent applications*)
    2.12 +    Finite_Lattice
    2.13 +    List_lexord
    2.14      Prefix_Order
    2.15 -    Rewrite
    2.16 -    (*conflicting type class instantiations*)
    2.17 -    List_lexord
    2.18 -    Sublist_Order
    2.19      Product_Lexorder
    2.20      Product_Order
    2.21 -    Finite_Lattice
    2.22 +    Sublist_Order
    2.23      (*data refinements and dependent applications*)
    2.24      AList_Mapping
    2.25      Code_Binary_Nat
    2.26 @@ -54,11 +50,13 @@
    2.27      DAList_Multiset
    2.28      RBT_Mapping
    2.29      RBT_Set
    2.30 +    (*prototypic tools*)
    2.31 +    Predicate_Compile_Quickcheck
    2.32      (*legacy tools*)
    2.33 -    Refute
    2.34      Old_Datatype
    2.35      Old_Recdef
    2.36      Old_SMT
    2.37 +    Refute
    2.38    document_files "root.bib" "root.tex"
    2.39  
    2.40  session "HOL-Hahn_Banach" in Hahn_Banach = HOL +