src/HOL/Library/Library.thy
author krauss
Mon Feb 26 21:34:16 2007 +0100 (2007-02-26)
changeset 22359 94a794672c8b
parent 21635 32f3e1127de2
child 22519 eb70ed79dac7
permissions -rw-r--r--
Added formalization of size-change principle (experimental).
     1 (* $Id$ *)
     2 (*<*)
     3 theory Library
     4 imports
     5   AssocList
     6   BigO
     7   Binomial
     8   Char_ord
     9   Coinductive_List
    10   Commutative_Ring
    11   Continuity
    12   EfficientNat
    13   ExecutableRat
    14   ExecutableSet
    15   FuncSet
    16   GCD
    17   Infinite_Set
    18   MLString
    19   Multiset
    20   NatPair
    21   Nat_Infinity
    22   Nested_Environment
    23   OptionalSugar
    24   Parity
    25   Permutation
    26   Primes
    27   Quotient
    28   Ramsey
    29   State_Monad
    30   Size_Change_Termination
    31   While_Combinator
    32   Word
    33   Zorn
    34 begin
    35 end
    36 (*>*)