src/HOL/Library/Library.thy
author krauss
Tue Aug 02 11:52:57 2011 +0200 (2011-08-02)
changeset 44014 88bd7d74a2c1
parent 44013 5cfc1c36ae97
child 44227 78e033e8ba05
permissions -rw-r--r--
moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
     1 (*<*)
     2 theory Library
     3 imports
     4   Abstract_Rat
     5   AssocList
     6   BigO
     7   Binomial
     8   Bit
     9   Boolean_Algebra
    10   Char_ord
    11   Continuity
    12   ContNotDenum
    13   Convex
    14   Countable
    15   Cset_Monad
    16   Diagonalize
    17   Dlist_Cset
    18   Eval_Witness
    19   Extended_Nat
    20   Float
    21   Formal_Power_Series
    22   Fraction_Field
    23   FrechetDeriv
    24   Cset
    25   FuncSet
    26   Function_Algebras
    27   Fundamental_Theorem_Algebra
    28   Indicator_Function
    29   Infinite_Set
    30   Inner_Product
    31   Lattice_Algebras
    32   Lattice_Syntax
    33   ListVector
    34   List_Cset
    35   Kleene_Algebra
    36   Mapping
    37   Monad_Syntax
    38   More_List
    39   Multiset
    40   Nested_Environment
    41   Numeral_Type
    42   Old_Recdef
    43   OptionalSugar
    44   Option_ord
    45   Permutation
    46   Poly_Deriv
    47   Polynomial
    48   Preorder
    49   Product_Vector
    50   Quotient_List
    51   Quotient_Option
    52   Quotient_Product
    53   Quotient_Sum
    54   Quotient_Syntax
    55   Quotient_Type
    56   Ramsey
    57   Reflection
    58   RBT_Mapping
    59   Set_Algebras
    60   State_Monad
    61   Sum_of_Squares
    62   Transitive_Closure_Table
    63   Univ_Poly
    64   Wfrec
    65   While_Combinator
    66   Zorn
    67 begin
    68 end
    69 (*>*)