author  haftmann 
Sat, 06 Sep 2014 20:12:34 +0200  
changeset 58196  1b3fbfb85980 
parent 58110  019c0211ed1f 
child 58197  4fd7f47ead6c 
permissions  rwrr 
10253  1 
(*<*) 
15131  2 
theory Library 
15140  3 
imports 
51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
50134
diff
changeset

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

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

6 
Bit 
56942  7 
BNF_Axiomatization 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
24281
diff
changeset

8 
Boolean_Algebra 
21256  9 
Char_ord 
29026  10 
ContNotDenum 
36648  11 
Convex 
26170  12 
Countable 
55075  13 
Countable_Set_Type 
48427
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
48283
diff
changeset

14 
Debug 
50087  15 
Diagonal_Subsequence 
48283  16 
Dlist 
51542  17 
Extended 
18 
Extended_Nat 

19 
Extended_Real 

48028  20 
FinFun 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28668
diff
changeset

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

23 
Fraction_Field 
53953  24 
FSet 
21256  25 
FuncSet 
48188  26 
Function_Division 
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset

27 
Function_Growth 
29879  28 
Fundamental_Theorem_Algebra 
58196
1b3fbfb85980
theory about lexicographic ordering on functions
haftmann
parents:
58110
diff
changeset

29 
Fun_Lexorder 
37665  30 
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

31 
Infinite_Set 
29993  32 
Inner_Product 
51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
50134
diff
changeset

33 
IArray 
35032
7efe662e41b4
separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents:
34020
diff
changeset

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

35 
Lattice_Syntax 
57998
8b7508f848ef
rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
Andreas Lochbihler
parents:
57250
diff
changeset

36 
Lattice_Constructions 
26173  37 
ListVector 
56415  38 
Lubs_Glbs 
29708  39 
Mapping 
37790  40 
Monad_Syntax 
15131  41 
Multiset 
24332
e3a2b75b1cf9
boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents:
24281
diff
changeset

42 
Numeral_Type 
57025  43 
NthRoot_Limits 
15470  44 
OptionalSugar 
26232  45 
Option_ord 
56020
f92479477c52
introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
hoelzl
parents:
55159
diff
changeset

46 
Order_Continuity 
48427
571cb1df0768
library theories for debugging and parallel computing using code generation towards Isabelle/ML
haftmann
parents:
48283
diff
changeset

47 
Parallel 
15131  48 
Permutation 
44227
78e033e8ba05
get Library/Permutations.thy compiled and working again
huffman
parents:
44014
diff
changeset

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

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

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

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

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

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

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

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

59 
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

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

61 
Ramsey 
29650  62 
Reflection 
44818
27ba81ad0890
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
44561
diff
changeset

63 
Saturated 
38622  64 
Set_Algebras 
21256  65 
State_Monad 
51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
50134
diff
changeset

66 
Sublist 
41474  67 
Sum_of_Squares 
33649
854173fcd21c
added a tabled implementation of the reflexive transitive closure
bulwahn
parents:
33356
diff
changeset

68 
Transitive_Closure_Table 
57250  69 
Tree 
15131  70 
While_Combinator 
71 
begin 

10253  72 
end 
73 
(*>*) 