author  wenzelm 
Tue, 29 Apr 2014 13:29:05 +0200  
changeset 56781  f2eb0f22589f 
parent 56680  4e2a0d4e7a82 
child 56801  8dd9df88f647 
permissions  rwrr 
51397
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
51263
diff
changeset

1 
chapter HOL 
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
51263
diff
changeset

2 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

3 
session HOL (main) = Pure + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

4 
description {* 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

5 
Classical Higherorder Logic. 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

6 
*} 
48338  7 
options [document_graph] 
8 
theories Complex_Main 

48901
5e0455e29339
more basic file dependencies  no load command here;
wenzelm
parents:
48765
diff
changeset

9 
files 
5e0455e29339
more basic file dependencies  no load command here;
wenzelm
parents:
48765
diff
changeset

10 
"Tools/Quickcheck/Narrowing_Engine.hs" 
5e0455e29339
more basic file dependencies  no load command here;
wenzelm
parents:
48765
diff
changeset

11 
"Tools/Quickcheck/PNF_Narrowing_Engine.hs" 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

12 
document_files 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

13 
"root.bib" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

14 
"root.tex" 
48338  15 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

16 
session "HOLProofs" = Pure + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

17 
description {* 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

18 
HOLMain with explicit proof terms. 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

19 
*} 
52499  20 
options [document = false] 
52488
cd65ee49a8ba
discontinued system option "proofs"  global state of Proofterm.proofs is persistently compiled into HOLProofs image;
wenzelm
parents:
52424
diff
changeset

21 
theories Proofs (*sequential change of global flag!*) 
48338  22 
theories Main 
48901
5e0455e29339
more basic file dependencies  no load command here;
wenzelm
parents:
48765
diff
changeset

23 
files 
5e0455e29339
more basic file dependencies  no load command here;
wenzelm
parents:
48765
diff
changeset

24 
"Tools/Quickcheck/Narrowing_Engine.hs" 
5e0455e29339
more basic file dependencies  no load command here;
wenzelm
parents:
48765
diff
changeset

25 
"Tools/Quickcheck/PNF_Narrowing_Engine.hs" 
48338  26 

50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset

27 
session "HOLLibrary" (main) in Library = HOL + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

28 
description {* 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

29 
Classical Higherorder Logic  batteries included. 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

30 
*} 
48481  31 
theories 
32 
Library 

51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset

33 
(*conflicting type class instantiations*) 
48481  34 
List_lexord 
35 
Sublist_Order 

51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51093
diff
changeset

36 
Product_Lexorder 
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51093
diff
changeset

37 
Product_Order 
51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset

38 
Finite_Lattice 
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset

39 
(*data refinements and dependent applications*) 
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset

40 
AList_Mapping 
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset

41 
Code_Binary_Nat 
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset

42 
Code_Char 
55447  43 
Code_Prolog 
48481  44 
Code_Real_Approx_By_Float 
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
49985
diff
changeset

45 
Code_Target_Numeral 
51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset

46 
DAList 
54429
be1bc181bcde
explicit inclusion of data refinement theory into HOLLibrary session
haftmann
parents:
54193
diff
changeset

47 
DAList_Multiset 
51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset

48 
RBT_Mapping 
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset

49 
RBT_Set 
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset

50 
(*legacy tools*) 
49985
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49932
diff
changeset

51 
Refute 
51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset

52 
Old_Recdef 
48932
c6e679443adc
actual use of (sos remote_csdp) via ISABELLE_FULL_TEST;
wenzelm
parents:
48901
diff
changeset

53 
theories [condition = ISABELLE_FULL_TEST] 
c6e679443adc
actual use of (sos remote_csdp) via ISABELLE_FULL_TEST;
wenzelm
parents:
48901
diff
changeset

54 
Sum_of_Squares_Remote 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

55 
document_files "root.bib" "root.tex" 
48481  56 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

57 
session "HOLHahn_Banach" in Hahn_Banach = HOL + 
48481  58 
description {* 
59 
Author: Gertrud Bauer, TU Munich 

60 

61 
The HahnBanach theorem for real vector spaces. 

51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

62 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

63 
This is the proof of the HahnBanach theorem for real vectorspaces, 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

64 
following H. Heuser, Funktionalanalysis, p. 228 232. The HahnBanach 
55018
2a526bd279ed
moved 'Zorn' into 'Main', since it's a BNF dependency
blanchet
parents:
54961
diff
changeset

65 
theorem is one of the fundamental theorems of functional analysis. It is a 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

66 
conclusion of Zorn's lemma. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

67 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

68 
Two different formaulations of the theorem are presented, one for general 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

69 
real vectorspaces and its application to normed vectorspaces. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

70 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

71 
The theorem says, that every continous linearform, defined on arbitrary 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

72 
subspaces (not only onedimensional subspaces), can be extended to a 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

73 
continous linearform on the whole vectorspace. 
48481  74 
*} 
75 
options [document_graph] 

76 
theories Hahn_Banach 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

77 
document_files "root.bib" "root.tex" 
48481  78 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

79 
session "HOLInduct" in Induct = HOL + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

80 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

81 
Examples of (Co)Inductive Definitions. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

82 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

83 
Comb proves the ChurchRosser theorem for combinators (see 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

84 
http://www.cl.cam.ac.uk/ftp/papers/reports/TR396lcpgenericautomaticprooftools.ps.gz). 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

85 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

86 
Mutil is the famous Mutilated Chess Board problem (see 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

87 
http://www.cl.cam.ac.uk/ftp/papers/reports/TR394lcpmutilatedchessboard.dvi.gz). 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

88 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

89 
PropLog proves the completeness of a formalization of propositional logic 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

90 
(see 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

91 
HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312lcpsetII.ps.gz). 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

92 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

93 
Exp demonstrates the use of iterated inductive definitions to reason about 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

94 
mutually recursive relations. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

95 
*} 
48481  96 
theories [quick_and_dirty] 
97 
Common_Patterns 

98 
theories 

99 
QuoDataType 

100 
QuoNestedDataType 

101 
Term 

102 
SList 

103 
ABexp 

104 
Tree 

105 
Ordinals 

106 
Sigma_Algebra 

107 
Comb 

108 
PropLog 

109 
Com 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

110 
document_files "root.tex" 
48481  111 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

112 
session "HOLIMP" in IMP = HOL + 
50870
b8606dd29783
hardwired document_variants, to prevent HOLIMP's \snip choking on macros from isabellestags.sty;
wenzelm
parents:
50844
diff
changeset

113 
options [document_graph, document_variants=document] 
48481  114 
theories [document = false] 
55601  115 
"~~/src/Tools/Permanent_Interpretation" 
48481  116 
"~~/src/HOL/Library/While_Combinator" 
117 
"~~/src/HOL/Library/Char_ord" 

118 
"~~/src/HOL/Library/List_lexord" 

51625  119 
"~~/src/HOL/Library/Quotient_List" 
120 
"~~/src/HOL/Library/Extended" 

48481  121 
theories 
122 
BExp 

123 
ASM 

50050  124 
Finite_Reachable 
52394  125 
Denotational 
52400  126 
Compiler2 
48481  127 
Poly_Types 
128 
Sec_Typing 

129 
Sec_TypingT 

52726  130 
Def_Init_Big 
131 
Def_Init_Small 

132 
Fold 

48481  133 
Live 
134 
Live_True 

135 
Hoare_Examples 

52269  136 
VCG 
52282  137 
Hoare_Total 
48481  138 
Collecting1 
48765
fb1ed5230abc
special code with lists no longer necessary, use sets
nipkow
parents:
48738
diff
changeset

139 
Collecting_Examples 
48481  140 
Abs_Int_Tests 
141 
Abs_Int1_parity 

142 
Abs_Int1_const 

143 
Abs_Int3 

144 
"Abs_Int_ITP/Abs_Int1_parity_ITP" 

145 
"Abs_Int_ITP/Abs_Int1_const_ITP" 

146 
"Abs_Int_ITP/Abs_Int3_ITP" 

147 
"Abs_Int_Den/Abs_Int_den2" 

148 
Procs_Dyn_Vars_Dyn 

149 
Procs_Stat_Vars_Dyn 

150 
Procs_Stat_Vars_Stat 

151 
C_like 

152 
OO 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

153 
document_files "root.bib" "root.tex" 
48481  154 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

155 
session "HOLIMPP" in IMPP = HOL + 
48481  156 
description {* 
157 
Author: David von Oheimb 

158 
Copyright 1999 TUM 

51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

159 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

160 
IMPP  An imperative language with procedures. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

161 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

162 
This is an extension of IMP with local variables and mutually recursive 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

163 
procedures. For documentation see "Hoare Logic for Mutual Recursion and 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

164 
Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). 
48481  165 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

166 
options [document = false] 
48481  167 
theories EvenOdd 
168 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

169 
session "HOLImport" in Import = HOL + 
48481  170 
options [document_graph] 
171 
theories HOL_Light_Maps 

172 
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 

173 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

174 
session "HOLNumber_Theory" in Number_Theory = HOL + 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset

175 
description {* 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset

176 
Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler 
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
55663
diff
changeset

177 
Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity. 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset

178 
*} 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset

179 
options [document_graph] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset

180 
theories [document = false] 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset

181 
"~~/src/HOL/Library/FuncSet" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset

182 
"~~/src/HOL/Library/Multiset" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset

183 
"~~/src/HOL/Algebra/Ring" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset

184 
"~~/src/HOL/Algebra/FiniteProduct" 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset

185 
theories 
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset

186 
Pocklington 
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
55663
diff
changeset

187 
Gauss 
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset

188 
Number_Theory 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

189 
document_files 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

190 
"root.tex" 
48481  191 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

192 
session "HOLOld_Number_Theory" in Old_Number_Theory = HOL + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

193 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

194 
Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

195 
Theorem, Wilson's Theorem, Quadratic Reciprocity. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

196 
*} 
48481  197 
options [document_graph] 
198 
theories [document = false] 

199 
"~~/src/HOL/Library/Infinite_Set" 

200 
"~~/src/HOL/Library/Permutation" 

201 
theories 

202 
Fib 

203 
Factorization 

204 
Chinese 

205 
WilsonRuss 

206 
WilsonBij 

207 
Quadratic_Reciprocity 

208 
Primes 

209 
Pocklington 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

210 
document_files "root.tex" 
48481  211 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

212 
session "HOLHoare" in Hoare = HOL + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

213 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

214 
Verification of imperative programs (verification conditions are generated 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

215 
automatically from pre/post conditions and loop invariants). 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

216 
*} 
48481  217 
theories Hoare 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

218 
document_files "root.bib" "root.tex" 
48481  219 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

220 
session "HOLHoare_Parallel" in Hoare_Parallel = HOL + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

221 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

222 
Verification of sharedvariable imperative programs a la OwickiGries. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

223 
(verification conditions are generated automatically). 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

224 
*} 
48481  225 
options [document_graph] 
226 
theories Hoare_Parallel 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

227 
document_files "root.bib" "root.tex" 
48481  228 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

229 
session "HOLCodegenerator_Test" in Codegenerator_Test = "HOLLibrary" + 
48481  230 
options [document = false, document_graph = false, browser_info = false] 
51422
821a70e29e0b
proper formatting, to facilitate linebased diff;
wenzelm
parents:
51421
diff
changeset

231 
theories 
821a70e29e0b
proper formatting, to facilitate linebased diff;
wenzelm
parents:
51421
diff
changeset

232 
Generate 
821a70e29e0b
proper formatting, to facilitate linebased diff;
wenzelm
parents:
51421
diff
changeset

233 
Generate_Binary_Nat 
821a70e29e0b
proper formatting, to facilitate linebased diff;
wenzelm
parents:
51421
diff
changeset

234 
Generate_Target_Nat 
821a70e29e0b
proper formatting, to facilitate linebased diff;
wenzelm
parents:
51421
diff
changeset

235 
Generate_Efficient_Datastructures 
821a70e29e0b
proper formatting, to facilitate linebased diff;
wenzelm
parents:
51421
diff
changeset

236 
Generate_Pretty_Char 
48481  237 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

238 
session "HOLMetis_Examples" in Metis_Examples = HOL + 
48481  239 
description {* 
240 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

241 
Author: Jasmin Blanchette, TU Muenchen 

242 

243 
Testing Metis and Sledgehammer. 

244 
*} 

48679  245 
options [timeout = 3600, document = false] 
48481  246 
theories 
247 
Abstraction 

248 
Big_O 

249 
Binary_Tree 

250 
Clausification 

251 
Message 

252 
Proxies 

253 
Tarski 

254 
Trans_Closure 

255 
Sets 

256 

55072  257 
session "HOLNitpick_Examples" in Nitpick_Examples = HOL + 
48481  258 
description {* 
259 
Author: Jasmin Blanchette, TU Muenchen 

260 
Copyright 2009 

261 
*} 

48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

262 
options [document = false] 
48481  263 
theories [quick_and_dirty] Nitpick_Examples 
264 

50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset

265 
session "HOLAlgebra" (main) in Algebra = HOL + 
48481  266 
description {* 
267 
Author: Clemens Ballarin, started 24 September 1999 

268 

269 
The Isabelle Algebraic Library. 

270 
*} 

271 
options [document_graph] 

272 
theories [document = false] 

273 
(* Preliminaries from set and number theory *) 

274 
"~~/src/HOL/Library/FuncSet" 

55159
608c157d743d
Replacing the theory Library/Binomial by Number_Theory/Binomial
paulson <lp15@cam.ac.uk>
parents:
55123
diff
changeset

275 
"~~/src/HOL/Number_Theory/Primes" 
608c157d743d
Replacing the theory Library/Binomial by Number_Theory/Binomial
paulson <lp15@cam.ac.uk>
parents:
55123
diff
changeset

276 
"~~/src/HOL/Number_Theory/Binomial" 
48481  277 
"~~/src/HOL/Library/Permutation" 
278 
theories 

279 
(*** New development, based on explicit structures ***) 

280 
(* Groups *) 

281 
FiniteProduct (* Product operator for commutative groups *) 

282 
Sylow (* Sylow's theorem *) 

283 
Bij (* Automorphism Groups *) 

284 

285 
(* Rings *) 

286 
Divisibility (* Rings *) 

287 
IntRing (* Ideals and residue classes *) 

288 
UnivPoly (* Polynomials *) 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

289 
document_files "root.bib" "root.tex" 
48481  290 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

291 
session "HOLAuth" in Auth = HOL + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

292 
description {* 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

293 
A new approach to verifying authentication protocols. 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

294 
*} 
48481  295 
options [document_graph] 
296 
theories 

297 
Auth_Shared 

298 
Auth_Public 

299 
"Smartcard/Auth_Smartcard" 

300 
"Guard/Auth_Guard_Shared" 

301 
"Guard/Auth_Guard_Public" 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

302 
document_files "root.tex" 
48481  303 

51236
f301ad90c48b
more explicit session dependency, for improved parallel performance of HOLUNITY test session  NB: separate 'theories' sections are sequential;
wenzelm
parents:
51161
diff
changeset

304 
session "HOLUNITY" in UNITY = "HOLAuth" + 
48481  305 
description {* 
306 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

307 
Copyright 1998 University of Cambridge 

308 

51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

309 
Verifying security protocols using Chandy and Misra's UNITY formalism. 
48481  310 
*} 
311 
options [document_graph] 

312 
theories 

313 
(*Basic metatheory*) 

314 
"UNITY_Main" 

315 

316 
(*Simple examples: no composition*) 

317 
"Simple/Deadlock" 

318 
"Simple/Common" 

319 
"Simple/Network" 

320 
"Simple/Token" 

321 
"Simple/Channel" 

322 
"Simple/Lift" 

323 
"Simple/Mutex" 

324 
"Simple/Reach" 

325 
"Simple/Reachability" 

326 

327 
(*Verifying security protocols using UNITY*) 

328 
"Simple/NSP_Bad" 

329 

330 
(*Example of composition*) 

331 
"Comp/Handshake" 

332 

333 
(*Universal properties examples*) 

334 
"Comp/Counter" 

335 
"Comp/Counterc" 

336 
"Comp/Priority" 

337 

338 
"Comp/TimerArray" 

339 
"Comp/Progress" 

340 

341 
"Comp/Alloc" 

342 
"Comp/AllocImpl" 

343 
"Comp/Client" 

344 

345 
(*obsolete*) 

346 
"ELT" 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

347 
document_files "root.tex" 
48481  348 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

349 
session "HOLUnix" in Unix = HOL + 
48481  350 
options [print_mode = "no_brackets,no_type_brackets"] 
351 
theories Unix 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

352 
document_files "root.bib" "root.tex" 
48481  353 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

354 
session "HOLZF" in ZF = HOL + 
48481  355 
theories MainZF Games 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

356 
document_files "root.tex" 
48481  357 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

358 
session "HOLImperative_HOL" in Imperative_HOL = HOL + 
48481  359 
options [document_graph, print_mode = "iff,no_brackets"] 
360 
theories [document = false] 

361 
"~~/src/HOL/Library/Countable" 

362 
"~~/src/HOL/Library/Monad_Syntax" 

363 
"~~/src/HOL/Library/LaTeXsugar" 

364 
theories Imperative_HOL_ex 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

365 
document_files "root.bib" "root.tex" 
48481  366 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

367 
session "HOLDecision_Procs" in Decision_Procs = HOL + 
51544  368 
description {* 
369 
Various decision procedures, typically involving reflection. 

370 
*} 

48496
a7eed34cf219
added condition = ISABELLE_POLYML according to nosmlnj targets in IsaMakefile;
wenzelm
parents:
48493
diff
changeset

371 
options [condition = ISABELLE_POLYML, document = false] 
48481  372 
theories Decision_Procs 
373 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

374 
session "HOLProofsex" in "Proofs/ex" = "HOLProofs" + 
52499  375 
options [document = false, parallel_proofs = 0] 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
52400
diff
changeset

376 
theories 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
52400
diff
changeset

377 
Hilbert_Classical 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
52400
diff
changeset

378 
XML_Data 
48481  379 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

380 
session "HOLProofsExtraction" in "Proofs/Extraction" = "HOLProofs" + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

381 
description {* 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

382 
Examples for program extraction in HigherOrder Logic. 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

383 
*} 
52499  384 
options [condition = ISABELLE_POLYML, parallel_proofs = 0] 
48481  385 
theories [document = false] 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51115
diff
changeset

386 
"~~/src/HOL/Library/Code_Target_Numeral" 
48481  387 
"~~/src/HOL/Library/Monad_Syntax" 
388 
"~~/src/HOL/Number_Theory/Primes" 

389 
"~~/src/HOL/Number_Theory/UniqueFactorization" 

390 
"~~/src/HOL/Library/State_Monad" 

391 
theories 

392 
Greatest_Common_Divisor 

393 
Warshall 

394 
Higman_Extraction 

395 
Pigeonhole 

396 
Euclid 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

397 
document_files "root.bib" "root.tex" 
48481  398 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

399 
session "HOLProofsLambda" in "Proofs/Lambda" = "HOLProofs" + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

400 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

401 
Lambda Calculus in de Bruijn's Notation. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

402 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

403 
This session defines lambdacalculus terms with de Bruijn indixes and 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

404 
proves confluence of beta, eta and beta+eta. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

405 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

406 
The paper "More ChurchRosser Proofs (in Isabelle/HOL)" describes the whole 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

407 
theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

408 
*} 
52499  409 
options [document_graph, print_mode = "no_brackets", parallel_proofs = 0] 
48481  410 
theories [document = false] 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51115
diff
changeset

411 
"~~/src/HOL/Library/Code_Target_Int" 
48481  412 
theories 
413 
Eta 

414 
StrongNorm 

415 
Standardization 

416 
WeakNorm 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

417 
document_files "root.bib" "root.tex" 
48481  418 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

419 
session "HOLProlog" in Prolog = HOL + 
48481  420 
description {* 
421 
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) 

51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

422 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

423 
A barebones implementation of LambdaProlog. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

424 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

425 
This is a simple exploratory implementation of LambdaProlog in HOL, 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

426 
including some minimal examples (in Test.thy) and a more typical example of 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

427 
a little functional language and its type system. 
48481  428 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

429 
options [document = false] 
48481  430 
theories Test Type 
431 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

432 
session "HOLMicroJava" in MicroJava = HOL + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

433 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

434 
Formalization of a fragment of Java, together with a corresponding virtual 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

435 
machine and a specification of its bytecode verifier and a lightweight 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

436 
bytecode verifier, including proofs of typesafety. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

437 
*} 
48481  438 
options [document_graph] 
439 
theories [document = false] "~~/src/HOL/Library/While_Combinator" 

440 
theories MicroJava 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

441 
document_files 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

442 
"introduction.tex" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

443 
"root.bib" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

444 
"root.tex" 
48481  445 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

446 
session "HOLNanoJava" in NanoJava = HOL + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

447 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

448 
Hoare Logic for a tiny fragment of Java. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

449 
*} 
48481  450 
options [document_graph] 
451 
theories Example 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

452 
document_files "root.bib" "root.tex" 
48481  453 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

454 
session "HOLBali" in Bali = HOL + 
48481  455 
options [document_graph] 
456 
theories 

457 
AxExample 

458 
AxSound 

459 
AxCompl 

460 
Trans 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

461 
document_files "root.tex" 
48481  462 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

463 
session "HOLIOA" in IOA = HOL + 
48481  464 
description {* 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

465 
Author: Tobias Nipkow and Konrad Slind and Olaf Müller 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

466 
Copyright 19941996 TU Muenchen 
48481  467 

55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55370
diff
changeset

468 
The metatheory of I/OAutomata in HOL. This formalization has been 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

469 
significantly changed and extended, see HOLCF/IOA. There are also the 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

470 
proofs of two communication protocols which formerly have been here. 
48481  471 

472 
@inproceedings{NipkowSlindIOA, 

473 
author={Tobias Nipkow and Konrad Slind}, 

474 
title={{I/O} Automata in {Isabelle/HOL}}, 

475 
booktitle={Proc.\ TYPES Workshop 1994}, 

476 
publisher=Springer, 

477 
series=LNCS, 

478 
note={To appear}} 

479 
ftp://ftp.informatik.tumuenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz 

480 

481 
and 

482 

483 
@inproceedings{MuellerNipkow, 

484 
author={Olaf M\"uller and Tobias Nipkow}, 

485 
title={Combining Model Checking and Deduction for {I/O}Automata}, 

486 
booktitle={Proc.\ TACAS Workshop}, 

487 
organization={Aarhus University, BRICS report}, 

488 
year=1995} 

489 
ftp://ftp.informatik.tumuenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz 

490 
*} 

48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

491 
options [document = false] 
48481  492 
theories Solve 
493 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

494 
session "HOLLattice" in Lattice = HOL + 
48481  495 
description {* 
496 
Author: Markus Wenzel, TU Muenchen 

497 

498 
Basic theory of lattices and orders. 

499 
*} 

500 
theories CompleteLattice 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

501 
document_files "root.tex" 
48481  502 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

503 
session "HOLex" in ex = HOL + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

504 
description {* 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

505 
Miscellaneous examples for HigherOrder Logic. 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

506 
*} 
48679  507 
options [timeout = 3600, condition = ISABELLE_POLYML] 
48481  508 
theories [document = false] 
509 
"~~/src/HOL/Library/State_Monad" 

50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
49985
diff
changeset

510 
Code_Binary_Nat_examples 
48481  511 
"~~/src/HOL/Library/FuncSet" 
512 
Eval_Examples 

513 
Normalization_by_Evaluation 

514 
Hebrew 

515 
Chinese 

516 
Serbian 

517 
"~~/src/HOL/Library/FinFun_Syntax" 

49985
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49932
diff
changeset

518 
"~~/src/HOL/Library/Refute" 
55123
a389b50e6a42
no document for Cartouche_Examples: avoid problems typesetting "\001";
wenzelm
parents:
55075
diff
changeset

519 
Cartouche_Examples 
48481  520 
theories 
521 
Iff_Oracle 

522 
Coercion_Examples 

523 
Higher_Order_Logic 

524 
Abstract_NAT 

525 
Guess 

526 
Fundefs 

527 
Induction_Schema 

528 
LocaleTest2 

529 
Records 

530 
While_Combinator_Example 

531 
MonoidGroup 

532 
BinEx 

533 
Hex_Bin_Examples 

534 
Antiquote 

535 
Multiquote 

536 
PER 

537 
NatSum 

538 
ThreeDivides 

539 
Intuitionistic 

540 
CTL 

541 
Arith_Examples 

542 
BT 

543 
Tree23 

544 
MergeSort 

545 
Lagrange 

546 
Groebner_Examples 

547 
MT 

548 
Unification 

549 
Primrec 

550 
Tarski 

551 
Classical 

552 
Set_Theory 

553 
Termination 

554 
Coherent 

555 
PresburgerEx 

51093  556 
Reflection_Examples 
48481  557 
Sqrt 
558 
Sqrt_Script 

559 
Transfer_Ex 

560 
Transfer_Int_Nat 

561 
HarmonicSeries 

562 
Refute_Examples 

563 
Execute_Choice 

564 
Gauge_Integration 

565 
Dedekind_Real 

566 
Quicksort 

567 
Birthday_Paradox 

568 
List_to_Set_Comprehension_Examples 

569 
Seq 

570 
Simproc_Tests 

571 
Executable_Relation 

572 
FinFunPred 

55663  573 
Set_Comprehension_Pointfree_Examples 
48481  574 
Parallel_Example 
50138  575 
IArray_Examples 
51559  576 
SVC_Oracle 
53430  577 
Simps_Case_Conv_Examples 
53935  578 
ML 
51558
91f8bed6d0a4
allow build with skip_proofs enabled  disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents:
51553
diff
changeset

579 
theories [skip_proofs = false] 
91f8bed6d0a4
allow build with skip_proofs enabled  disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents:
51553
diff
changeset

580 
Meson_Test 
48690  581 
theories [condition = SVC_HOME] 
582 
svc_test 

48481  583 
theories [condition = ZCHAFF_HOME] 
584 
(*requires zChaff (or some other reasonably fast SAT solver)*) 

585 
Sudoku 

586 
(* FIXME 

587 
(*requires a proofgenerating SAT solver (zChaff or MiniSAT)*) 

55240  588 
SAT_Examples 
48481  589 
*) 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

590 
document_files "root.bib" "root.tex" 
48481  591 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

592 
session "HOLIsar_Examples" in Isar_Examples = HOL + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

593 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

594 
Miscellaneous Isabelle/Isar examples for HigherOrder Logic. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

595 
*} 
48481  596 
theories [document = false] 
597 
"~~/src/HOL/Library/Lattice_Syntax" 

598 
"../Number_Theory/Primes" 

599 
theories 

600 
Basic_Logic 

601 
Cantor 

602 
Drinker 

603 
Expr_Compiler 

604 
Fibonacci 

605 
Group 

606 
Group_Context 

607 
Group_Notepad 

608 
Hoare_Ex 

609 
Knaster_Tarski 

610 
Mutilated_Checkerboard 

611 
Nested_Datatype 

612 
Peirce 

613 
Puzzle 

614 
Summation 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

615 
document_files 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

616 
"root.bib" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

617 
"root.tex" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

618 
"style.tex" 
48481  619 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

620 
session "HOLSET_Protocol" in SET_Protocol = HOL + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

621 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

622 
Verification of the SET Protocol. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

623 
*} 
48481  624 
options [document_graph] 
625 
theories [document = false] "~~/src/HOL/Library/Nat_Bijection" 

626 
theories SET_Protocol 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

627 
document_files "root.tex" 
48481  628 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

629 
session "HOLMatrix_LP" in Matrix_LP = HOL + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

630 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

631 
Twodimensional matrices and linear programming. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

632 
*} 
48481  633 
options [document_graph] 
634 
theories Cplex 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

635 
document_files "root.tex" 
48481  636 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

637 
session "HOLTLA" in TLA = HOL + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

638 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

639 
Lamport's Temporal Logic of Actions. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

640 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

641 
options [document = false] 
48481  642 
theories TLA 
643 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

644 
session "HOLTLAInc" in "TLA/Inc" = "HOLTLA" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

645 
options [document = false] 
48481  646 
theories Inc 
647 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

648 
session "HOLTLABuffer" in "TLA/Buffer" = "HOLTLA" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

649 
options [document = false] 
48481  650 
theories DBuffer 
651 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

652 
session "HOLTLAMemory" in "TLA/Memory" = "HOLTLA" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

653 
options [document = false] 
48481  654 
theories MemoryImplementation 
655 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

656 
session "HOLTPTP" in TPTP = HOL + 
48481  657 
description {* 
658 
Author: Jasmin Blanchette, TU Muenchen 

659 
Author: Nik Sultana, University of Cambridge 

660 
Copyright 2011 

661 

662 
TPTPrelated extensions. 

663 
*} 

48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

664 
options [document = false] 
48481  665 
theories 
666 
ATP_Theory_Export 

667 
MaSh_Eval 

668 
MaSh_Export 

669 
TPTP_Interpret 

670 
THF_Arith 

55596
928b9f677165
reconstruction framework for LEOII's TPTP proofs;
sultana
parents:
55450
diff
changeset

671 
TPTP_Proof_Reconstruction 
52488
cd65ee49a8ba
discontinued system option "proofs"  global state of Proofterm.proofs is persistently compiled into HOLProofs image;
wenzelm
parents:
52424
diff
changeset

672 
theories 
48481  673 
ATP_Problem_Import 
674 

50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset

675 
session "HOLMultivariate_Analysis" (main) in Multivariate_Analysis = HOL + 
48481  676 
options [document_graph] 
677 
theories 

678 
Multivariate_Analysis 

679 
Determinants 

56215  680 
PolyRoots 
681 
Complex_Analysis_Basics 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

682 
document_files 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

683 
"root.tex" 
48481  684 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

685 
session "HOLProbability" in "Probability" = "HOLMultivariate_Analysis" + 
48617  686 
options [document_graph] 
48481  687 
theories [document = false] 
688 
"~~/src/HOL/Library/Countable" 

689 
"~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits" 

690 
"~~/src/HOL/Library/Permutation" 

691 
theories 

692 
Probability 

693 
"ex/Dining_Cryptographers" 

694 
"ex/Koepf_Duermuth_Countermeasure" 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

695 
document_files "root.tex" 
48481  696 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

697 
session "HOLNominal" (main) in Nominal = HOL + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

698 
options [document = false] 
48481  699 
theories Nominal 
700 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

701 
session "HOLNominalExamples" in "Nominal/Examples" = "HOLNominal" + 
48679  702 
options [timeout = 3600, condition = ISABELLE_POLYML, document = false] 
48481  703 
theories Nominal_Examples 
704 
theories [quick_and_dirty] VC_Condition 

705 

55054
e1f3714bc508
moved subset of 'HOLCardinals' needed for BNF into 'HOL'
blanchet
parents:
55033
diff
changeset

706 
session "HOLCardinals" in Cardinals = HOL + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

707 
description {* 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

708 
Ordinals and Cardinals, Full Theories. 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

709 
*} 
49511
9f5bfef8bd82
created separate session "HOLBNFLFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents:
49510
diff
changeset

710 
options [document = false] 
49439  711 
theories Cardinals 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

712 
document_files 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

713 
"intro.tex" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

714 
"root.tex" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

715 
"root.bib" 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset

716 

55071  717 
session "HOLBNF_Examples" in BNF_Examples = HOL + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

718 
description {* 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

719 
Examples for Bounded Natural Functors. 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

720 
*} 
49932
9d3bc26485eb
back to parallel HOLBNFExamples, which seems to have suffered from Future.map on canceled persistent futures;
wenzelm
parents:
49903
diff
changeset

721 
options [document = false] 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset

722 
theories 
56454  723 
Compat 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset

724 
Lambda_Term 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset

725 
Process 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset

726 
TreeFsetI 
49872  727 
"Derivation_Trees/Gram_Lang" 
728 
"Derivation_Trees/Parallel" 

50517  729 
Koenig 
54961  730 
Stream_Processor 
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset

731 
Misc_Codatatype 
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset

732 
Misc_Datatype 
54193  733 
Misc_Primcorec 
53306  734 
Misc_Primrec 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset

735 

50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset

736 
session "HOLWord" (main) in Word = HOL + 
48481  737 
options [document_graph] 
738 
theories Word 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

739 
document_files "root.bib" "root.tex" 
48481  740 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

741 
session "HOLWordExamples" in "Word/Examples" = "HOLWord" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

742 
options [document = false] 
48481  743 
theories WordExamples 
744 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

745 
session "HOLStatespace" in Statespace = HOL + 
51558
91f8bed6d0a4
allow build with skip_proofs enabled  disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents:
51553
diff
changeset

746 
theories [skip_proofs = false] 
91f8bed6d0a4
allow build with skip_proofs enabled  disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents:
51553
diff
changeset

747 
StateSpaceEx 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

748 
document_files "root.tex" 
48481  749 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

750 
session "HOLNSA" in NSA = HOL + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

751 
description {* 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

752 
Nonstandard analysis. 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

753 
*} 
48481  754 
options [document_graph] 
755 
theories Hypercomplex 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

756 
document_files "root.tex" 
48481  757 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

758 
session "HOLNSAExamples" in "NSA/Examples" = "HOLNSA" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

759 
options [document = false] 
48481  760 
theories NSPrimes 
761 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

762 
session "HOLMirabelle" in Mirabelle = HOL + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

763 
options [document = false] 
48481  764 
theories Mirabelle_Test 
48589
fb446a780d50
separate session HOLMirabelleex  cannot run isolated shell scripts within build tool;
wenzelm
parents:
48588
diff
changeset

765 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

766 
session "HOLMirabelleex" in "Mirabelle/ex" = "HOLMirabelle" + 
49448
8a232a4e3fd8
reactivate HOLMirabelleex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
wenzelm
parents:
49439
diff
changeset

767 
options [document = false, timeout = 60] 
8a232a4e3fd8
reactivate HOLMirabelleex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
wenzelm
parents:
49439
diff
changeset

768 
theories Ex 
48481  769 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

770 
session "HOLWordSMT_Examples" in SMT_Examples = "HOLWord" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

771 
options [document = false, quick_and_dirty] 
48481  772 
theories 
52722  773 
Boogie 
48481  774 
SMT_Examples 
775 
SMT_Word_Examples 

50666
6f48853f08d5
actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
blanchet
parents:
50665
diff
changeset

776 
theories [condition = ISABELLE_FULL_TEST] 
6f48853f08d5
actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
blanchet
parents:
50665
diff
changeset

777 
SMT_Tests 
48481  778 
files 
779 
"Boogie_Dijkstra.certs" 

780 
"Boogie_Max.certs" 

52722  781 
"SMT_Examples.certs" 
56079
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55973
diff
changeset

782 
"SMT_Examples.certs2" 
175ac95720d4
use 'smt2' in SMT examples as much as currently possible
blanchet
parents:
55973
diff
changeset

783 
"SMT_Word_Examples.certs2" 
48481  784 
"VCC_Max.certs" 
785 

50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset

786 
session "HOLSPARK" (main) in "SPARK" = "HOLWord" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

787 
options [document = false] 
48481  788 
theories SPARK 
789 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

790 
session "HOLSPARKExamples" in "SPARK/Examples" = "HOLSPARK" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

791 
options [document = false] 
48481  792 
theories 
793 
"Gcd/Greatest_Common_Divisor" 

794 

795 
"Liseq/Longest_Increasing_Subsequence" 

796 

797 
"RIPEMD160/F" 

798 
"RIPEMD160/Hash" 

799 
"RIPEMD160/K_L" 

800 
"RIPEMD160/K_R" 

801 
"RIPEMD160/R_L" 

802 
"RIPEMD160/Round" 

803 
"RIPEMD160/R_R" 

804 
"RIPEMD160/S_L" 

805 
"RIPEMD160/S_R" 

806 

807 
"Sqrt/Sqrt" 

808 
files 

809 
"Gcd/greatest_common_divisor/g_c_d.fdl" 

810 
"Gcd/greatest_common_divisor/g_c_d.rls" 

811 
"Gcd/greatest_common_divisor/g_c_d.siv" 

812 
"Liseq/liseq/liseq_length.fdl" 

813 
"Liseq/liseq/liseq_length.rls" 

814 
"Liseq/liseq/liseq_length.siv" 

815 
"RIPEMD160/rmd/f.fdl" 

816 
"RIPEMD160/rmd/f.rls" 

817 
"RIPEMD160/rmd/f.siv" 

818 
"RIPEMD160/rmd/hash.fdl" 

819 
"RIPEMD160/rmd/hash.rls" 

820 
"RIPEMD160/rmd/hash.siv" 

821 
"RIPEMD160/rmd/k_l.fdl" 

822 
"RIPEMD160/rmd/k_l.rls" 

823 
"RIPEMD160/rmd/k_l.siv" 

824 
"RIPEMD160/rmd/k_r.fdl" 

825 
"RIPEMD160/rmd/k_r.rls" 

826 
"RIPEMD160/rmd/k_r.siv" 

827 
"RIPEMD160/rmd/r_l.fdl" 

828 
"RIPEMD160/rmd/r_l.rls" 

829 
"RIPEMD160/rmd/r_l.siv" 

830 
"RIPEMD160/rmd/round.fdl" 

831 
"RIPEMD160/rmd/round.rls" 

832 
"RIPEMD160/rmd/round.siv" 

833 
"RIPEMD160/rmd/r_r.fdl" 

834 
"RIPEMD160/rmd/r_r.rls" 

835 
"RIPEMD160/rmd/r_r.siv" 

836 
"RIPEMD160/rmd/s_l.fdl" 

837 
"RIPEMD160/rmd/s_l.rls" 

838 
"RIPEMD160/rmd/s_l.siv" 

839 
"RIPEMD160/rmd/s_r.fdl" 

840 
"RIPEMD160/rmd/s_r.rls" 

841 
"RIPEMD160/rmd/s_r.siv" 

842 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

843 
session "HOLSPARKManual" in "SPARK/Manual" = "HOLSPARK" + 
48486  844 
options [show_question_marks = false] 
48481  845 
theories 
846 
Example_Verification 

847 
VC_Principles 

848 
Reference 

849 
Complex_Types 

850 
files 

851 
"complex_types_app/initialize.fdl" 

852 
"complex_types_app/initialize.rls" 

853 
"complex_types_app/initialize.siv" 

854 
"loop_invariant/proc1.fdl" 

855 
"loop_invariant/proc1.rls" 

856 
"loop_invariant/proc1.siv" 

857 
"loop_invariant/proc2.fdl" 

858 
"loop_invariant/proc2.rls" 

859 
"loop_invariant/proc2.siv" 

860 
"simple_greatest_common_divisor/g_c_d.fdl" 

861 
"simple_greatest_common_divisor/g_c_d.rls" 

862 
"simple_greatest_common_divisor/g_c_d.siv" 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

863 
document_files 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

864 
"complex_types.ads" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

865 
"complex_types_app.adb" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

866 
"complex_types_app.ads" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

867 
"Gcd.adb" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

868 
"Gcd.ads" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

869 
"intro.tex" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

870 
"loop_invariant.adb" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

871 
"loop_invariant.ads" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

872 
"root.bib" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

873 
"root.tex" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

874 
"Simple_Gcd.adb" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

875 
"Simple_Gcd.ads" 
48481  876 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

877 
session "HOLMutabelle" in Mutabelle = HOL + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

878 
options [document = false] 
48481  879 
theories MutabelleExtra 
880 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

881 
session "HOLQuickcheck_Examples" in Quickcheck_Examples = HOL + 
50179
978200ae8473
timeout in proper place (HOLQuickcheck_Examples approx. 1min, HOLQuickcheck_Benchmark approx. 1h);
wenzelm
parents:
50161
diff
changeset

882 
options [document = false] 
48588  883 
theories 
48690  884 
Quickcheck_Examples 
885 
(* FIXME 

886 
Quickcheck_Lattice_Examples 

887 
Completeness 

888 
Quickcheck_Interfaces 

889 
Hotel_Example *) 

48598  890 
theories [condition = ISABELLE_GHC] 
891 
Quickcheck_Narrowing_Examples 

48588  892 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

893 
session "HOLQuickcheck_Benchmark" in Quickcheck_Benchmark = HOL + 
50571
b649e33e4821
HOLQuickcheck_Benchmark works without timeout (NB: isatest imposes global timeout already);
wenzelm
parents:
50568
diff
changeset

894 
theories [condition = ISABELLE_FULL_TEST, quick_and_dirty] 
50568
ee090b5712f3
reverting d466ebc27810 as the previous changeset should allow to run Find_Unused_Assms_Examples again
bulwahn
parents:
50517
diff
changeset

895 
Find_Unused_Assms_Examples 
48618
1f7e068b4613
moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents:
48614
diff
changeset

896 
Needham_Schroeder_No_Attacker_Example 
1f7e068b4613
moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents:
48614
diff
changeset

897 
Needham_Schroeder_Guided_Attacker_Example 
48690  898 
Needham_Schroeder_Unguided_Attacker_Example 
48481  899 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

900 
session "HOLQuotient_Examples" in Quotient_Examples = HOL + 
48481  901 
description {* 
902 
Author: Cezary Kaliszyk and Christian Urban 

903 
*} 

48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

904 
options [document = false] 
48481  905 
theories 
906 
DList 

907 
FSet 

908 
Quotient_Int 

909 
Quotient_Message 

910 
Lift_FSet 

911 
Lift_Set 

912 
Lift_Fun 

913 
Quotient_Rat 

914 
Lift_DList 

53682
1b55aeda0e46
include Int_Pow into Quotient_Examples; add end of the theory
kuncar
parents:
53430
diff
changeset

915 
Int_Pow 
48481  916 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

917 
session "HOLPredicate_Compile_Examples" in Predicate_Compile_Examples = HOL + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

918 
options [document = false] 
48690  919 
theories 
48481  920 
Examples 
921 
Predicate_Compile_Tests 

48690  922 
(* FIXME 
923 
Predicate_Compile_Quickcheck_Examples  should be added again soon (since 21Oct2010) *) 

48481  924 
Specialisation_Examples 
48690  925 
IMP_1 
926 
IMP_2 

55450
9eddc17749f7
reactivate some examples that still appear to work;
wenzelm
parents:
55447
diff
changeset

927 
(* FIXME since 21Jul2011 
9eddc17749f7
reactivate some examples that still appear to work;
wenzelm
parents:
55447
diff
changeset

928 
Hotel_Example_Small_Generator 
48690  929 
IMP_3 
930 
IMP_4 *) 

55450
9eddc17749f7
reactivate some examples that still appear to work;
wenzelm
parents:
55447
diff
changeset

931 
theories [condition = "ISABELLE_SWIPL"] 
48690  932 
Code_Prolog_Examples 
933 
Context_Free_Grammar_Example 

934 
Hotel_Example_Prolog 

935 
Lambda_Example 

936 
List_Examples 

55450
9eddc17749f7
reactivate some examples that still appear to work;
wenzelm
parents:
55447
diff
changeset

937 
theories [condition = "ISABELLE_SWIPL", quick_and_dirty] 
48690  938 
Reg_Exp_Example 
48481  939 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

940 
session HOLCF (main) in HOLCF = HOL + 
48338  941 
description {* 
942 
Author: Franz Regensburger 

943 
Author: Brian Huffman 

944 

945 
HOLCF  a semantic extension of HOL by the LCF logic. 

946 
*} 

947 
options [document_graph] 

48470
7483aa690b4f
clarified "document" again, eliminated redundant "no_document";
wenzelm
parents:
48458
diff
changeset

948 
theories [document = false] 
48338  949 
"~~/src/HOL/Library/Nat_Bijection" 
950 
"~~/src/HOL/Library/Countable" 

48481  951 
theories 
952 
Plain_HOLCF 

953 
Fixrec 

954 
HOLCF 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

955 
document_files "root.tex" 
48481  956 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

957 
session "HOLCFTutorial" in "HOLCF/Tutorial" = HOLCF + 
48481  958 
theories 
959 
Domain_ex 

960 
Fixrec_ex 

961 
New_Domain 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

962 
document_files "root.tex" 
48481  963 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

964 
session "HOLCFLibrary" in "HOLCF/Library" = HOLCF + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

965 
options [document = false] 
48481  966 
theories HOLCF_Library 
967 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

968 
session "HOLCFIMP" in "HOLCF/IMP" = HOLCF + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

969 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

970 
IMP  A WHILElanguage and its Semantics. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

971 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

972 
This is the HOLCFbased denotational semantics of a simple WHILElanguage. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

973 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

974 
options [document = false] 
48481  975 
theories HoareEx 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

976 
document_files "root.tex" 
48338  977 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

978 
session "HOLCFex" in "HOLCF/ex" = HOLCF + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

979 
description {* 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

980 
Miscellaneous examples for HOLCF. 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

981 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

982 
options [document = false] 
48481  983 
theories 
984 
Dnat 

985 
Dagstuhl 

986 
Focus_ex 

987 
Fix2 

988 
Hoare 

989 
Concurrency_Monad 

990 
Loop 

991 
Powerdomain_ex 

992 
Domain_Proofs 

993 
Letrec 

994 
Pattern_Match 

995 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

996 
session "HOLCFFOCUS" in "HOLCF/FOCUS" = HOLCF + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

997 
description {* 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

998 
FOCUS: a theory of streamprocessing functions Isabelle/HOLCF. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

999 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1000 
For introductions to FOCUS, see 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1001 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1002 
"The Design of Distributed Systems  An Introduction to FOCUS" 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1003 
http://www4.in.tum.de/publ/html.php?e=2 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1004 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1005 
"Specification and Refinement of a Buffer of Length One" 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1006 
http://www4.in.tum.de/publ/html.php?e=15 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1007 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1008 
"Specification and Development of Interactive Systems: Focus on Streams, 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1009 
Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1010 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

1011 
options [document = false] 
48481  1012 
theories 
1013 
Fstreams 

1014 
FOCUS 

1015 
Buffer_adm 

1016 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

1017 
session IOA in "HOLCF/IOA" = HOLCF + 
48481  1018 
description {* 
1019 
Author: Olaf Mueller 

51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1020 
Copyright 1997 TU München 
48481  1021 

51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1022 
A formalization of I/O automata in HOLCF. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1023 

2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1024 
The distribution contains simulation relations, temporal logic, and an 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1025 
abstraction theory. Everything is based upon a domaintheoretic model of 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1026 
finite and infinite sequences. 
48481  1027 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

1028 
options [document = false] 
48481  1029 
theories "meta_theory/Abstraction" 
1030 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

1031 
session "IOAABP" in "HOLCF/IOA/ABP" = IOA + 
48481  1032 
description {* 
1033 
Author: Olaf Mueller 

1034 

1035 
The Alternating Bit Protocol performed in I/OAutomata. 

1036 
*} 

48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

1037 
options [document = false] 
48481  1038 
theories Correctness 
1039 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

1040 
session "IOANTP" in "HOLCF/IOA/NTP" = IOA + 
48481  1041 
description {* 
1042 
Author: Tobias Nipkow & Konrad Slind 

1043 

1044 
A network transmission protocol, performed in the 

1045 
I/O automata formalization by Olaf Mueller. 

1046 
*} 

48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

1047 
options [document = false] 
48481  1048 
theories Correctness 
1049 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

1050 
session "IOAStorage" in "HOLCF/IOA/Storage" = IOA + 
48481  1051 
description {* 
1052 
Author: Olaf Mueller 

1053 

1054 
Memory storage case study. 

1055 
*} 

48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

1056 
options [document = false] 
48481  1057 
theories Correctness 
1058 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

1059 
session "IOAex" in "HOLCF/IOA/ex" = IOA + 
48481  1060 
description {* 
1061 
Author: Olaf Mueller 

1062 
*} 

48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

1063 
options [document = false] 
48481  1064 
theories 
1065 
TrivEx 

1066 
TrivEx2 

1067 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

1068 
session "HOLDatatype_Benchmark" in Datatype_Benchmark = HOL + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

1069 
description {* 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

1070 
Some rather large datatype examples (from John Harrison). 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

1071 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

1072 
options [document = false] 
48635  1073 
theories [condition = ISABELLE_FULL_TEST, timing] 
48481  1074 
Brackin 
1075 
Instructions 

1076 
SML 

1077 
Verilog 

1078 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

1079 
session "HOLRecord_Benchmark" in Record_Benchmark = HOL + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

1080 
description {* 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

1081 
Some benchmark on large record. 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

1082 
*} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

1083 
options [document = false] 
48635  1084 
theories [condition = ISABELLE_FULL_TEST, timing] 
48481  1085 
Record_Benchmark 
1086 