src/HOL/Library/Library.thy
author haftmann
Wed Aug 15 08:57:40 2007 +0200 (2007-08-15)
changeset 24281 7d0334b69711
parent 24197 c9e3cb5e5681
child 24332 e3a2b75b1cf9
permissions -rw-r--r--
added Eval_Witness theory
wenzelm@20809
     1
(* $Id$ *)
wenzelm@10253
     2
(*<*)
nipkow@15131
     3
theory Library
nipkow@15140
     4
imports
haftmann@24197
     5
  Abstract_Rat
wenzelm@21256
     6
  AssocList
avigad@16908
     7
  BigO
wenzelm@21256
     8
  Binomial
wenzelm@21256
     9
  Char_ord
wenzelm@21256
    10
  Coinductive_List
wenzelm@21256
    11
  Commutative_Ring
nipkow@15131
    12
  Continuity
haftmann@23854
    13
  Efficient_Nat
haftmann@22519
    14
  Eval
haftmann@24281
    15
  Eval_Witness
haftmann@23854
    16
  Executable_Rat
chaieb@22981
    17
  Executable_Real
haftmann@23854
    18
  Executable_Set
wenzelm@21256
    19
  FuncSet
wenzelm@21256
    20
  GCD
wenzelm@21256
    21
  Infinite_Set
haftmann@23854
    22
  ML_String
nipkow@15131
    23
  Multiset
nipkow@15131
    24
  NatPair
nipkow@15131
    25
  Nat_Infinity
nipkow@15131
    26
  Nested_Environment
nipkow@15470
    27
  OptionalSugar
wenzelm@21256
    28
  Parity
nipkow@15131
    29
  Permutation
haftmann@22799
    30
  Pretty_Char_chr
haftmann@22799
    31
  Pretty_Int
nipkow@15131
    32
  Primes
nipkow@15131
    33
  Quotient
krauss@21635
    34
  Ramsey
wenzelm@21256
    35
  State_Monad
krauss@22359
    36
  Size_Change_Termination
nipkow@15131
    37
  While_Combinator
nipkow@15131
    38
  Word
nipkow@15131
    39
  Zorn
nipkow@15131
    40
begin
wenzelm@10253
    41
end
wenzelm@10253
    42
(*>*)