src/HOL/Library/Library.thy
author immler
Thu Nov 15 10:49:58 2012 +0100 (2012-11-15)
changeset 50087 635d73673b5e
parent 48742 28d59ce5ebfd
child 50134 13211e07d931
permissions -rw-r--r--
regularity of measures, therefore:
characterization of closure with infimum distance;
characterize of compact sets as totally bounded;
added Diagonal_Subsequence to Library;
introduced (enumerable) topological basis;
rational boxes as basis of ordered euclidean space;
moved some lemmas upwards
     1 (*<*)
     2 theory Library
     3 imports
     4   Abstract_Rat
     5   AList_Mapping
     6   BigO
     7   Binomial
     8   Bit
     9   Boolean_Algebra
    10   Char_ord
    11   Continuity
    12   ContNotDenum
    13   Convex
    14   Countable
    15   Debug
    16   Diagonal_Subsequence
    17   Dlist
    18   Eval_Witness
    19   Extended_Nat
    20   FinFun
    21   Float
    22   Formal_Power_Series
    23   Fraction_Field
    24   FrechetDeriv
    25   FuncSet
    26   Function_Division
    27   Fundamental_Theorem_Algebra
    28   Indicator_Function
    29   Infinite_Set
    30   Inner_Product
    31   Lattice_Algebras
    32   Lattice_Syntax
    33   ListVector
    34   Kleene_Algebra
    35   Mapping
    36   Monad_Syntax
    37   Multiset
    38   Numeral_Type
    39   Old_Recdef
    40   OptionalSugar
    41   Option_ord
    42   Parallel
    43   Permutation
    44   Permutations
    45   Poly_Deriv
    46   Polynomial
    47   Preorder
    48   Product_Vector
    49   Quotient_List
    50   Quotient_Option
    51   Quotient_Product
    52   Quotient_Set
    53   Quotient_Sum
    54   Quotient_Syntax
    55   Quotient_Type
    56   Ramsey
    57   Reflection
    58   RBT_Mapping
    59   (* RBT_Set *) (* FIXME not included because it breaks Codegenerator_Test/Generate*.thy *)
    60   Saturated
    61   Set_Algebras
    62   State_Monad
    63   Sum_of_Squares
    64   Transitive_Closure_Table
    65   Univ_Poly
    66   Wfrec
    67   While_Combinator
    68   Zorn
    69 begin
    70 end
    71 (*>*)