src/HOL/Library/Library.thy
author Andreas Lochbihler
Tue Dec 01 12:35:11 2015 +0100 (2015-12-01)
changeset 61766 507b39df1a57
parent 61178 0b071f72f330
child 62352 35a9e1cbb5b3
permissions -rw-r--r--
add formalisation of Bourbaki-Witt fixpoint theorem
     1 (*<*)
     2 theory Library
     3 imports
     4   AList
     5   BigO
     6   Bit
     7   BNF_Axiomatization
     8   Boolean_Algebra
     9   Bourbaki_Witt_Fixpoint
    10   Char_ord
    11   Code_Test
    12   ContNotDenum
    13   Convex
    14   Countable
    15   Countable_Set_Type
    16   Debug
    17   Diagonal_Subsequence
    18   Disjoint_Sets
    19   Dlist
    20   Extended
    21   Extended_Nat
    22   Extended_Real
    23   FinFun
    24   Float
    25   Formal_Power_Series
    26   Fraction_Field
    27   FSet
    28   FuncSet
    29   Function_Division
    30   Function_Growth
    31   Fundamental_Theorem_Algebra
    32   Fun_Lexorder
    33   Groups_Big_Fun
    34   Indicator_Function
    35   Infinite_Set
    36   Inner_Product
    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   Numeral_Type
    49   Omega_Words_Fun
    50   OptionalSugar
    51   Option_ord
    52   Order_Continuity
    53   Parallel
    54   Permutation
    55   Permutations
    56   Poly_Deriv
    57   Polynomial
    58   Preorder
    59   Product_Vector
    60   Quadratic_Discriminant
    61   Quotient_List
    62   Quotient_Option
    63   Quotient_Product
    64   Quotient_Set
    65   Quotient_Sum
    66   Quotient_Syntax
    67   Quotient_Type
    68   Ramsey
    69   Reflection
    70   Saturated
    71   Set_Algebras
    72   State_Monad
    73   Stream
    74   Sublist
    75   Sum_of_Squares
    76   Transitive_Closure_Table
    77   Tree_Multiset
    78   While_Combinator
    79 begin
    80 end
    81 (*>*)