author  chaieb 
Tue, 15 May 2007 18:28:02 +0200  
changeset 22981  cf071f3fc4ae 
parent 22799  ed7d53db2170 
child 23100  1c84d7294d5b 
permissions  rwrr 
20809  1 
(* $Id$ *) 
10253  2 
(*<*) 
15131  3 
theory Library 
15140  4 
imports 
21256  5 
AssocList 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
16109
diff
changeset

6 
BigO 
21256  7 
Binomial 
8 
Char_ord 

9 
Coinductive_List 

10 
Commutative_Ring 

15131  11 
Continuity 
15324  12 
EfficientNat 
22519  13 
Eval 
21256  14 
ExecutableRat 
22981
cf071f3fc4ae
A verified theory for rational numbers representation and simple calculations;
chaieb
parents:
22799
diff
changeset

15 
Executable_Real 
17633  16 
ExecutableSet 
21256  17 
FuncSet 
18 
GCD 

19 
Infinite_Set 

20400  20 
MLString 
15131  21 
Multiset 
22 
NatPair 

23 
Nat_Infinity 

24 
Nested_Environment 

15470  25 
OptionalSugar 
21256  26 
Parity 
15131  27 
Permutation 
22799
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22519
diff
changeset

28 
Pretty_Char_chr 
ed7d53db2170
moved code generation pretty integers and characters to separate theories
haftmann
parents:
22519
diff
changeset

29 
Pretty_Int 
15131  30 
Primes 
31 
Quotient 

21635
32f3e1127de2
added Ramsey.thy to Library imports, to include it in the daily builds
krauss
parents:
21256
diff
changeset

32 
Ramsey 
21256  33 
State_Monad 
22359
94a794672c8b
Added formalization of sizechange principle (experimental).
krauss
parents:
21635
diff
changeset

34 
Size_Change_Termination 
15131  35 
While_Combinator 
36 
Word 

37 
Zorn 

38 
begin 

10253  39 
end 
40 
(*>*) 