src/HOL/Library/Library.thy
author Christian Sternagel
Thu Dec 13 13:11:38 2012 +0100 (2012-12-13)
changeset 50516 ed6b40d15d1c
parent 50134 13211e07d931
child 51161 6ed12ae3b3e1
permissions -rw-r--r--
renamed "emb" to "list_hembeq";
make "list_hembeq" reflexive independent of the base order;
renamed "sub" to "sublisteq";
dropped "transp_on" (state transitivity explicitly instead);
no need to hide "sub" after renaming;
replaced some ASCII symbols by proper Isabelle symbols;
NEWS
     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   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   Lattice_Algebras
    33   Lattice_Syntax
    34   ListVector
    35   Kleene_Algebra
    36   Mapping
    37   Monad_Syntax
    38   Multiset
    39   Numeral_Type
    40   Old_Recdef
    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   RBT_Mapping
    60   (* RBT_Set *) (* FIXME not included because it breaks Codegenerator_Test/Generate*.thy *)
    61   Saturated
    62   Set_Algebras
    63   State_Monad
    64   Sum_of_Squares
    65   Transitive_Closure_Table
    66   Univ_Poly
    67   Wfrec
    68   While_Combinator
    69   Zorn
    70 begin
    71 end
    72 (*>*)