src/HOL/Library/Library.thy
author haftmann
Sun Oct 08 22:28:19 2017 +0200 (2017-10-08)
changeset 66797 9c9baae29217
parent 66563 87b9eb69d5ba
child 67224 341fbce5b26d
permissions -rw-r--r--
removed mere toy example from library
     1 (*<*)
     2 theory Library
     3 imports
     4   AList
     5   BigO
     6   Bit
     7   BNF_Axiomatization
     8   BNF_Corec
     9   Boolean_Algebra
    10   Bourbaki_Witt_Fixpoint
    11   Char_ord
    12   Code_Test
    13   Combine_PER
    14   Complete_Partial_Order2
    15   Countable
    16   Countable_Complete_Lattices
    17   Countable_Set_Type
    18   Debug
    19   Diagonal_Subsequence
    20   Discrete
    21   Disjoint_Sets
    22   Dlist
    23   Extended
    24   Extended_Nat
    25   Extended_Nonnegative_Real
    26   Extended_Real
    27   Finite_Map
    28   Float
    29   FSet
    30   FuncSet
    31   Function_Division
    32   Fun_Lexorder
    33   Going_To_Filter
    34   Groups_Big_Fun
    35   Indicator_Function
    36   Infinite_Set
    37   IArray
    38   Lattice_Algebras
    39   Lattice_Syntax
    40   Lattice_Constructions
    41   Linear_Temporal_Logic_on_Streams
    42   ListVector
    43   Lub_Glb
    44   Mapping
    45   Monad_Syntax
    46   More_List
    47   Multiset_Order
    48   Multiset_Permutations
    49   Nonpos_Ints
    50   Numeral_Type
    51   Omega_Words_Fun
    52   Open_State_Syntax
    53   Option_ord
    54   Order_Continuity
    55   Parallel
    56   Pattern_Aliases
    57   Periodic_Fun
    58   Perm
    59   Permutation
    60   Permutations
    61   Preorder
    62   Product_Plus
    63   Quadratic_Discriminant
    64   Quotient_List
    65   Quotient_Option
    66   Quotient_Product
    67   Quotient_Set
    68   Quotient_Sum
    69   Quotient_Syntax
    70   Quotient_Type
    71   Ramsey
    72   Reflection
    73   Rewrite
    74   Saturated
    75   Set_Algebras
    76   State_Monad
    77   Stirling
    78   Stream
    79   Sublist
    80   Sum_of_Squares
    81   Transitive_Closure_Table
    82   Tree_Multiset
    83   Tree_Real
    84   Type_Length
    85   Uprod
    86   While_Combinator
    87 begin
    88 end
    89 (*>*)