author  bulwahn 
Mon, 12 Sep 2011 10:57:58 +0200  
changeset 44897  787983a08bfb 
parent 44818  27ba81ad0890 
child 45074  04286b0fc856 
permissions  rwrr 
10253  1 
(*<*) 
15131  2 
theory Library 
15140  3 
imports 
27652
818666de6c24
refined code generator setup for rational numbers; more simplification rules for rational numbers
haftmann
parents:
27475
diff
changeset

4 
Abstract_Rat 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
44818
diff
changeset

5 
AList_Mapping 
16908
d374530bfaaa
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
avigad
parents:
16109
diff
changeset

6 
BigO 
21256  7 
Binomial 
29994
6ca6b6bd6e15
add formalization of a type of integers mod 2 to Library
huffman
parents:
29993
diff
changeset

8 
Bit 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
24281
diff
changeset

9 
Boolean_Algebra 
21256  10 
Char_ord 
15131  11 
Continuity 
29026  12 
ContNotDenum 
36648  13 
Convex 
26170  14 
Countable 
43976
af17d7934116
Add theory for setting up monad syntax for Cset
Andreas Lochbihler
parents:
43958
diff
changeset

15 
Cset_Monad 
30326
a01b2de0e3e1
constructive version of Cantor's first diagonalization argument
haftmann
parents:
30261
diff
changeset

16 
Diagonalize 
43146  17 
Dlist_Cset 
24281  18 
Eval_Witness 
43919  19 
Extended_Nat 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28668
diff
changeset

20 
Float 
29688  21 
Formal_Power_Series 
31761
3585bebe49a8
Added Library/Fraction_Field.thy: The fraction field of any integral
chaieb
parents:
31379
diff
changeset

22 
Fraction_Field 
29986  23 
FrechetDeriv 
40672
abd4e7358847
replaced misleading Fset/fset name  these do not stand for finite sets
haftmann
parents:
40349
diff
changeset

24 
Cset 
21256  25 
FuncSet 
38622  26 
Function_Algebras 
29879  27 
Fundamental_Theorem_Algebra 
37665  28 
Indicator_Function 
27475
61b979a2c820
add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)
huffman
parents:
27368
diff
changeset

29 
Infinite_Set 
29993  30 
Inner_Product 
35032
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
34020
diff
changeset

31 
Lattice_Algebras 
30326
a01b2de0e3e1
constructive version of Cantor's first diagonalization argument
haftmann
parents:
30261
diff
changeset

32 
Lattice_Syntax 
26173  33 
ListVector 
31990  34 
Kleene_Algebra 
29708  35 
Mapping 
37790  36 
Monad_Syntax 
37023  37 
More_List 
15131  38 
Multiset 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
24281
diff
changeset

39 
Numeral_Type 
44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
43976
diff
changeset

40 
Old_Recdef 
15470  41 
OptionalSugar 
26232  42 
Option_ord 
15131  43 
Permutation 
44227
78e033e8ba05
get Library/Permutations.thy compiled and working again
huffman
parents:
44014
diff
changeset

44 
Permutations 
29985
57975b45ab70
split polynomialrelated stuff from Deriv.thy into Library/Poly_Deriv.thy
huffman
parents:
29879
diff
changeset

45 
Poly_Deriv 
29987  46 
Polynomial 
31060
75d7c7cc8bdb
added theory for explicit equivalence relation in preorders
haftmann
parents:
30326
diff
changeset

47 
Preorder 
30019
a2f19e0a28b2
add theory of products as real vector spaces to Library
huffman
parents:
30018
diff
changeset

48 
Product_Vector 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35100
diff
changeset

49 
Quotient_List 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35100
diff
changeset

50 
Quotient_Option 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35100
diff
changeset

51 
Quotient_Product 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35100
diff
changeset

52 
Quotient_Sum 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35100
diff
changeset

53 
Quotient_Syntax 
35100
53754ec7360b
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
wenzelm
parents:
35091
diff
changeset

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

55 
Ramsey 
29650  56 
Reflection 
43124  57 
RBT_Mapping 
44818
27ba81ad0890
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
44561
diff
changeset

58 
Saturated 
38622  59 
Set_Algebras 
21256  60 
State_Monad 
41474  61 
Sum_of_Squares 
33649
854173fcd21c
added a tabled implementation of the reflexive transitive closure
bulwahn
parents:
33356
diff
changeset

62 
Transitive_Closure_Table 
29504  63 
Univ_Poly 
44014
88bd7d74a2c1
moved recursion combinator to HOL/Library/Wfrec.thy  it is so fundamental and wellknown that it should survive recdef
krauss
parents:
44013
diff
changeset

64 
Wfrec 
15131  65 
While_Combinator 
27475
61b979a2c820
add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)
huffman
parents:
27368
diff
changeset

66 
Zorn 
15131  67 
begin 
10253  68 
end 
69 
(*>*) 