src/HOL/Library/Library.thy
author haftmann
Fri Feb 15 11:47:34 2013 +0100 (2013-02-15)
changeset 51161 6ed12ae3b3e1
parent 50134 13211e07d931
child 51174 071674018df9
permissions -rw-r--r--
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
four different code generation tests for different code setup constellations;
augment code generation setup where necessary
     1 (*<*)
     2 theory Library
     3 imports
     4   Abstract_Rat
     5   AList
     6   BigO
     7   Binomial
     8   Bit
     9   Boolean_Algebra
    10   Char_ord
    11   Continuity
    12   ContNotDenum
    13   Convex
    14   Countable
    15   Countable_Set
    16   Debug
    17   Diagonal_Subsequence
    18   Dlist
    19   Eval_Witness
    20   Extended_Nat
    21   FinFun
    22   Float
    23   Formal_Power_Series
    24   Fraction_Field
    25   FrechetDeriv
    26   FuncSet
    27   Function_Division
    28   Fundamental_Theorem_Algebra
    29   Indicator_Function
    30   Infinite_Set
    31   Inner_Product
    32   IArray
    33   Lattice_Algebras
    34   Lattice_Syntax
    35   ListVector
    36   Kleene_Algebra
    37   Mapping
    38   Monad_Syntax
    39   Multiset
    40   Numeral_Type
    41   OptionalSugar
    42   Option_ord
    43   Parallel
    44   Permutation
    45   Permutations
    46   Poly_Deriv
    47   Polynomial
    48   Preorder
    49   Product_Vector
    50   Quotient_List
    51   Quotient_Option
    52   Quotient_Product
    53   Quotient_Set
    54   Quotient_Sum
    55   Quotient_Syntax
    56   Quotient_Type
    57   Ramsey
    58   Reflection
    59   Saturated
    60   Set_Algebras
    61   State_Monad
    62   Sublist
    63   Sum_of_Squares
    64   Transitive_Closure_Table
    65   Univ_Poly
    66   Wfrec
    67   While_Combinator
    68   Zorn
    69 begin
    70 end
    71 (*>*)