src/HOL/Library/Library.thy
author haftmann
Fri Nov 01 18:51:14 2013 +0100 (2013-11-01)
changeset 54230 b1d955791529
parent 54220 0e6645622f22
child 54545 483131676087
permissions -rw-r--r--
more simplification rules on unary and binary minus
     1 (*<*)
     2 theory Library
     3 imports
     4   AList
     5   BigO
     6   Binomial
     7   Bit
     8   Boolean_Algebra
     9   Char_ord
    10   Continuity
    11   ContNotDenum
    12   Convex
    13   Countable
    14   Countable_Set
    15   Debug
    16   Diagonal_Subsequence
    17   Dlist
    18   Extended
    19   Extended_Nat
    20   Extended_Real
    21   FinFun
    22   Float
    23   Formal_Power_Series
    24   Fraction_Field
    25   FSet
    26   FuncSet
    27   Function_Division
    28   Function_Growth
    29   Fundamental_Theorem_Algebra
    30   Indicator_Function
    31   Infinite_Set
    32   Inner_Product
    33   IArray
    34   Lattice_Algebras
    35   Lattice_Syntax
    36   ListVector
    37   Kleene_Algebra
    38   Mapping
    39   Monad_Syntax
    40   Multiset
    41   Numeral_Type
    42   OptionalSugar
    43   Option_ord
    44   Order_Union
    45   Parallel
    46   Permutation
    47   Permutations
    48   Poly_Deriv
    49   Polynomial
    50   Preorder
    51   Product_Vector
    52   Quotient_List
    53   Quotient_Option
    54   Quotient_Product
    55   Quotient_Set
    56   Quotient_Sum
    57   Quotient_Syntax
    58   Quotient_Type
    59   Ramsey
    60   Reflection
    61   Saturated
    62   Set_Algebras
    63   State_Monad
    64   Sublist
    65   Sum_of_Squares
    66   Transitive_Closure_Table
    67   Wfrec
    68   While_Combinator
    69   Zorn
    70 begin
    71 end
    72 (*>*)