author  wenzelm 
Tue, 12 Mar 2013 21:59:48 +0100  
changeset 51403  2ff3a5589b05 
parent 51397  03b586ee5930 
child 51421  b5d559b101d9 
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 + 
48338  4 
description {* Classical Higherorder Logic *} 
5 
options [document_graph] 

6 
theories Complex_Main 

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

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

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

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

10 
"document/root.bib" 
5e0455e29339
more basic file dependencies  no load command here;
wenzelm
parents:
48765
diff
changeset

11 
"document/root.tex" 
48338  12 

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

13 
session "HOLProofs" = Pure + 
48509  14 
description {* HOLMain with explicit proof terms *} 
50988  15 
options [document = false, proofs = 2] 
48338  16 
theories Main 
48901
5e0455e29339
more basic file dependencies  no load command here;
wenzelm
parents:
48765
diff
changeset

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

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

19 
"Tools/Quickcheck/PNF_Narrowing_Engine.hs" 
48338  20 

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

21 
session "HOLLibrary" (main) in Library = HOL + 
48481  22 
description {* Classical Higherorder Logic  batteries included *} 
23 
theories 

24 
Library 

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

25 
(*conflicting type class instantiations*) 
48481  26 
List_lexord 
27 
Sublist_Order 

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

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

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

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

31 
(*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

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

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

34 
Code_Char 
48721  35 
(* Code_Prolog FIXME cf. 76965c356d2a *) 
48481  36 
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

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

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

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

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

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

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

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

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

45 
Sum_of_Squares_Remote 
48481  46 
files "document/root.bib" "document/root.tex" 
47 

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

48 
session "HOLHahn_Banach" in Hahn_Banach = HOL + 
48481  49 
description {* 
50 
Author: Gertrud Bauer, TU Munich 

51 

52 
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

53 

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

54 
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

55 
following H. Heuser, Funktionalanalysis, p. 228 232. The HahnBanach 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

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

57 
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

58 

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

59 
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

60 
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

61 

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

62 
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

63 
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

64 
continous linearform on the whole vectorspace. 
48481  65 
*} 
66 
options [document_graph] 

67 
theories Hahn_Banach 

68 
files "document/root.bib" "document/root.tex" 

69 

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

70 
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

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

72 
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

73 

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

74 
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

75 
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

76 

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

77 
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

78 
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

79 

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

80 
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

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

82 
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

83 

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

84 
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

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

86 
*} 
48481  87 
theories [quick_and_dirty] 
88 
Common_Patterns 

89 
theories 

90 
QuoDataType 

91 
QuoNestedDataType 

92 
Term 

93 
SList 

94 
ABexp 

95 
Tree 

96 
Ordinals 

97 
Sigma_Algebra 

98 
Comb 

99 
PropLog 

100 
Com 

101 
files "document/root.tex" 

102 

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

103 
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

104 
options [document_graph, document_variants=document] 
48481  105 
theories [document = false] 
106 
"~~/src/HOL/ex/Interpretation_with_Defs" 

107 
"~~/src/HOL/Library/While_Combinator" 

108 
"~~/src/HOL/Library/Char_ord" 

109 
"~~/src/HOL/Library/List_lexord" 

110 
theories 

111 
BExp 

112 
ASM 

50050  113 
Finite_Reachable 
48481  114 
Denotation 
115 
Comp_Rev 

116 
Poly_Types 

117 
Sec_Typing 

118 
Sec_TypingT 

50161  119 
Def_Init_Sound_Big 
120 
Def_Init_Sound_Small 

48481  121 
Live 
122 
Live_True 

123 
Hoare_Examples 

124 
VC 

125 
HoareT 

126 
Collecting1 

48765
fb1ed5230abc
special code with lists no longer necessary, use sets
nipkow
parents:
48738
diff
changeset

127 
Collecting_Examples 
48481  128 
Abs_Int_Tests 
129 
Abs_Int1_parity 

130 
Abs_Int1_const 

131 
Abs_Int3 

132 
"Abs_Int_ITP/Abs_Int1_parity_ITP" 

133 
"Abs_Int_ITP/Abs_Int1_const_ITP" 

134 
"Abs_Int_ITP/Abs_Int3_ITP" 

135 
"Abs_Int_Den/Abs_Int_den2" 

136 
Procs_Dyn_Vars_Dyn 

137 
Procs_Stat_Vars_Dyn 

138 
Procs_Stat_Vars_Stat 

139 
C_like 

140 
OO 

141 
Fold 

142 
files "document/root.bib" "document/root.tex" 

143 

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

144 
session "HOLIMPP" in IMPP = HOL + 
48481  145 
description {* 
146 
Author: David von Oheimb 

147 
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

148 

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

149 
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

150 

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

151 
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

152 
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

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

155 
options [document = false] 
48481  156 
theories EvenOdd 
157 

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

158 
session "HOLImport" in Import = HOL + 
48481  159 
options [document_graph] 
160 
theories HOL_Light_Maps 

161 
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 

162 

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

163 
session "HOLNumber_Theory" in Number_Theory = HOL + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

164 
options [document = false] 
48481  165 
theories Number_Theory 
166 

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

167 
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

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

169 
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

170 
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

171 
*} 
48481  172 
options [document_graph] 
173 
theories [document = false] 

174 
"~~/src/HOL/Library/Infinite_Set" 

175 
"~~/src/HOL/Library/Permutation" 

176 
theories 

177 
Fib 

178 
Factorization 

179 
Chinese 

180 
WilsonRuss 

181 
WilsonBij 

182 
Quadratic_Reciprocity 

183 
Primes 

184 
Pocklington 

185 
files "document/root.tex" 

186 

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

187 
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

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

189 
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

190 
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

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

192 

48481  193 
theories Hoare 
194 
files "document/root.bib" "document/root.tex" 

195 

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

196 
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

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

198 
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

199 
(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

200 
*} 
48481  201 
options [document_graph] 
202 
theories Hoare_Parallel 

203 
files "document/root.bib" "document/root.tex" 

204 

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

205 
session "HOLCodegenerator_Test" in Codegenerator_Test = "HOLLibrary" + 
48481  206 
options [document = false, document_graph = false, browser_info = false] 
51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset

207 
theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Generate_Pretty_Char 
48481  208 

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

209 
session "HOLMetis_Examples" in Metis_Examples = HOL + 
48481  210 
description {* 
211 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

212 
Author: Jasmin Blanchette, TU Muenchen 

213 

214 
Testing Metis and Sledgehammer. 

215 
*} 

48679  216 
options [timeout = 3600, document = false] 
48481  217 
theories 
218 
Abstraction 

219 
Big_O 

220 
Binary_Tree 

221 
Clausification 

222 
Message 

223 
Proxies 

224 
Tarski 

225 
Trans_Closure 

226 
Sets 

227 

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

228 
session "HOLNitpick_Examples" in Nitpick_Examples = HOL + 
48481  229 
description {* 
230 
Author: Jasmin Blanchette, TU Muenchen 

231 
Copyright 2009 

232 
*} 

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

233 
options [document = false] 
48481  234 
theories [quick_and_dirty] Nitpick_Examples 
235 

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

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

239 

240 
The Isabelle Algebraic Library. 

241 
*} 

242 
options [document_graph] 

243 
theories [document = false] 

244 
(* Preliminaries from set and number theory *) 

245 
"~~/src/HOL/Library/FuncSet" 

246 
"~~/src/HOL/Old_Number_Theory/Primes" 

247 
"~~/src/HOL/Library/Binomial" 

248 
"~~/src/HOL/Library/Permutation" 

249 
theories 

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

251 
(* Groups *) 

252 
FiniteProduct (* Product operator for commutative groups *) 

253 
Sylow (* Sylow's theorem *) 

254 
Bij (* Automorphism Groups *) 

255 

256 
(* Rings *) 

257 
Divisibility (* Rings *) 

258 
IntRing (* Ideals and residue classes *) 

259 
UnivPoly (* Polynomials *) 

260 
theories [document = false] 

261 
(*** Old development, based on axiomatic type classes ***) 

262 
"abstract/Abstract" (*The ring theory*) 

263 
"poly/Polynomial" (*The full theory*) 

264 
files "document/root.bib" "document/root.tex" 

265 

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

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

267 
description {* A new approach to verifying authentication protocols. *} 
48481  268 
options [document_graph] 
269 
theories 

270 
Auth_Shared 

271 
Auth_Public 

272 
"Smartcard/Auth_Smartcard" 

273 
"Guard/Auth_Guard_Shared" 

274 
"Guard/Auth_Guard_Public" 

275 
files "document/root.tex" 

276 

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

277 
session "HOLUNITY" in UNITY = "HOLAuth" + 
48481  278 
description {* 
279 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

280 
Copyright 1998 University of Cambridge 

281 

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

282 
Verifying security protocols using Chandy and Misra's UNITY formalism. 
48481  283 
*} 
284 
options [document_graph] 

285 
theories 

286 
(*Basic metatheory*) 

287 
"UNITY_Main" 

288 

289 
(*Simple examples: no composition*) 

290 
"Simple/Deadlock" 

291 
"Simple/Common" 

292 
"Simple/Network" 

293 
"Simple/Token" 

294 
"Simple/Channel" 

295 
"Simple/Lift" 

296 
"Simple/Mutex" 

297 
"Simple/Reach" 

298 
"Simple/Reachability" 

299 

300 
(*Verifying security protocols using UNITY*) 

301 
"Simple/NSP_Bad" 

302 

303 
(*Example of composition*) 

304 
"Comp/Handshake" 

305 

306 
(*Universal properties examples*) 

307 
"Comp/Counter" 

308 
"Comp/Counterc" 

309 
"Comp/Priority" 

310 

311 
"Comp/TimerArray" 

312 
"Comp/Progress" 

313 

314 
"Comp/Alloc" 

315 
"Comp/AllocImpl" 

316 
"Comp/Client" 

317 

318 
(*obsolete*) 

319 
"ELT" 

320 
files "document/root.tex" 

321 

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

322 
session "HOLUnix" in Unix = HOL + 
48481  323 
options [print_mode = "no_brackets,no_type_brackets"] 
324 
theories Unix 

325 
files "document/root.bib" "document/root.tex" 

326 

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

327 
session "HOLZF" in ZF = HOL + 
48481  328 
theories MainZF Games 
329 
files "document/root.tex" 

330 

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

331 
session "HOLImperative_HOL" in Imperative_HOL = HOL + 
48481  332 
options [document_graph, print_mode = "iff,no_brackets"] 
333 
theories [document = false] 

334 
"~~/src/HOL/Library/Countable" 

335 
"~~/src/HOL/Library/Monad_Syntax" 

336 
"~~/src/HOL/Library/LaTeXsugar" 

337 
theories Imperative_HOL_ex 

338 
files "document/root.bib" "document/root.tex" 

339 

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

340 
session "HOLDecision_Procs" in Decision_Procs = HOL + 
48496
a7eed34cf219
added condition = ISABELLE_POLYML according to nosmlnj targets in IsaMakefile;
wenzelm
parents:
48493
diff
changeset

341 
options [condition = ISABELLE_POLYML, document = false] 
48481  342 
theories Decision_Procs 
343 

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

344 
session "HOLProofsex" in "Proofs/ex" = "HOLProofs" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

345 
options [document = false, proofs = 2, parallel_proofs = 0] 
48481  346 
theories Hilbert_Classical 
347 

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

348 
session "HOLProofsExtraction" in "Proofs/Extraction" = "HOLProofs" + 
48481  349 
description {* Examples for program extraction in HigherOrder Logic *} 
48496
a7eed34cf219
added condition = ISABELLE_POLYML according to nosmlnj targets in IsaMakefile;
wenzelm
parents:
48493
diff
changeset

350 
options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0] 
48481  351 
theories [document = false] 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51115
diff
changeset

352 
"~~/src/HOL/Library/Code_Target_Numeral" 
48481  353 
"~~/src/HOL/Library/Monad_Syntax" 
354 
"~~/src/HOL/Number_Theory/Primes" 

355 
"~~/src/HOL/Number_Theory/UniqueFactorization" 

356 
"~~/src/HOL/Library/State_Monad" 

357 
theories 

358 
Greatest_Common_Divisor 

359 
Warshall 

360 
Higman_Extraction 

361 
Pigeonhole 

362 
Euclid 

363 
files "document/root.bib" "document/root.tex" 

364 

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

365 
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

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

367 
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

368 

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

369 
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

370 
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

371 

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

372 
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

373 
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

374 
*} 
48481  375 
options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0] 
376 
theories [document = false] 

51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51115
diff
changeset

377 
"~~/src/HOL/Library/Code_Target_Int" 
48481  378 
theories 
379 
Eta 

380 
StrongNorm 

381 
Standardization 

382 
WeakNorm 

383 
files "document/root.bib" "document/root.tex" 

384 

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

385 
session "HOLProlog" in Prolog = HOL + 
48481  386 
description {* 
387 
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

388 

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

389 
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

390 

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

391 
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

392 
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

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

395 
options [document = false] 
48481  396 
theories Test Type 
397 

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

398 
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

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

400 
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

401 
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

402 
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

403 
*} 
48481  404 
options [document_graph] 
405 
theories [document = false] "~~/src/HOL/Library/While_Combinator" 

406 
theories MicroJava 

407 
files 

408 
"document/introduction.tex" 

409 
"document/root.bib" 

410 
"document/root.tex" 

411 

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

412 
session "HOLMicroJavaskip_proofs" in MicroJava = HOL + 
48636  413 
options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs, quick_and_dirty] 
414 
theories MicroJava 

415 

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

416 
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

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

418 
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

419 
*} 
48481  420 
options [document_graph] 
421 
theories Example 

422 
files "document/root.bib" "document/root.tex" 

423 

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

424 
session "HOLBali" in Bali = HOL + 
48481  425 
options [document_graph] 
426 
theories 

427 
AxExample 

428 
AxSound 

429 
AxCompl 

430 
Trans 

431 
files "document/root.tex" 

432 

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

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

435 
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

436 
Copyright 19941996 TU Muenchen 
48481  437 

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

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

439 
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

440 
proofs of two communication protocols which formerly have been here. 
48481  441 

442 
@inproceedings{NipkowSlindIOA, 

443 
author={Tobias Nipkow and Konrad Slind}, 

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

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

446 
publisher=Springer, 

447 
series=LNCS, 

448 
note={To appear}} 

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

450 

451 
and 

452 

453 
@inproceedings{MuellerNipkow, 

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

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

456 
booktitle={Proc.\ TACAS Workshop}, 

457 
organization={Aarhus University, BRICS report}, 

458 
year=1995} 

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

460 
*} 

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

461 
options [document = false] 
48481  462 
theories Solve 
463 

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

464 
session "HOLLattice" in Lattice = HOL + 
48481  465 
description {* 
466 
Author: Markus Wenzel, TU Muenchen 

467 

468 
Basic theory of lattices and orders. 

469 
*} 

470 
theories CompleteLattice 

471 
files "document/root.tex" 

472 

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

473 
session "HOLex" in ex = HOL + 
48481  474 
description {* Miscellaneous examples for HigherOrder Logic. *} 
48679  475 
options [timeout = 3600, condition = ISABELLE_POLYML] 
48481  476 
theories [document = false] 
477 
"~~/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

478 
Code_Binary_Nat_examples 
48481  479 
"~~/src/HOL/Library/FuncSet" 
480 
Eval_Examples 

481 
Normalization_by_Evaluation 

482 
Hebrew 

483 
Chinese 

484 
Serbian 

485 
"~~/src/HOL/Library/FinFun_Syntax" 

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

486 
"~~/src/HOL/Library/Refute" 
48481  487 
theories 
488 
Iff_Oracle 

489 
Coercion_Examples 

490 
Numeral_Representation 

491 
Higher_Order_Logic 

492 
Abstract_NAT 

493 
Guess 

494 
Binary 

495 
Fundefs 

496 
Induction_Schema 

497 
LocaleTest2 

498 
Records 

499 
While_Combinator_Example 

500 
MonoidGroup 

501 
BinEx 

502 
Hex_Bin_Examples 

503 
Antiquote 

504 
Multiquote 

505 
PER 

506 
NatSum 

507 
ThreeDivides 

508 
Intuitionistic 

509 
CTL 

510 
Arith_Examples 

511 
BT 

512 
Tree23 

513 
MergeSort 

514 
Lagrange 

515 
Groebner_Examples 

516 
MT 

517 
Unification 

518 
Primrec 

519 
Tarski 

520 
Classical 

521 
Set_Theory 

522 
Meson_Test 

523 
Termination 

524 
Coherent 

525 
PresburgerEx 

51093  526 
Reflection_Examples 
48481  527 
Sqrt 
528 
Sqrt_Script 

529 
Transfer_Ex 

530 
Transfer_Int_Nat 

531 
HarmonicSeries 

532 
Refute_Examples 

533 
Execute_Choice 

534 
Summation 

535 
Gauge_Integration 

536 
Dedekind_Real 

537 
Quicksort 

538 
Birthday_Paradox 

539 
List_to_Set_Comprehension_Examples 

540 
Seq 

541 
Simproc_Tests 

542 
Executable_Relation 

543 
FinFunPred 

544 
Set_Comprehension_Pointfree_Tests 

545 
Parallel_Example 

50138  546 
IArray_Examples 
48481  547 
theories SVC_Oracle 
48690  548 
theories [condition = SVC_HOME] 
549 
svc_test 

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

552 
Sudoku 

553 
(* FIXME 

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

555 
(*global sideeffects ahead!*) 

556 
try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *) 

557 
*) 

558 
files "document/root.bib" "document/root.tex" 

559 

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

560 
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

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

562 
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

563 
*} 
48481  564 
theories [document = false] 
565 
"~~/src/HOL/Library/Lattice_Syntax" 

566 
"../Number_Theory/Primes" 

567 
theories 

568 
Basic_Logic 

569 
Cantor 

570 
Drinker 

571 
Expr_Compiler 

572 
Fibonacci 

573 
Group 

574 
Group_Context 

575 
Group_Notepad 

576 
Hoare_Ex 

577 
Knaster_Tarski 

578 
Mutilated_Checkerboard 

579 
Nested_Datatype 

580 
Peirce 

581 
Puzzle 

582 
Summation 

583 
files 

584 
"document/root.bib" 

585 
"document/root.tex" 

586 
"document/style.tex" 

587 

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

588 
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

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

590 
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

591 
*} 
48481  592 
options [document_graph] 
593 
theories [document = false] "~~/src/HOL/Library/Nat_Bijection" 

594 
theories SET_Protocol 

595 
files "document/root.tex" 

596 

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

597 
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

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

599 
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

600 
*} 
48481  601 
options [document_graph] 
602 
theories Cplex 

603 
files "document/root.tex" 

604 

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

605 
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

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

607 
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

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

609 
options [document = false] 
48481  610 
theories TLA 
611 

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

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

613 
options [document = false] 
48481  614 
theories Inc 
615 

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

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

617 
options [document = false] 
48481  618 
theories DBuffer 
619 

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

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

621 
options [document = false] 
48481  622 
theories MemoryImplementation 
623 

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

624 
session "HOLTPTP" in TPTP = HOL + 
48481  625 
description {* 
626 
Author: Jasmin Blanchette, TU Muenchen 

627 
Author: Nik Sultana, University of Cambridge 

628 
Copyright 2011 

629 

630 
TPTPrelated extensions. 

631 
*} 

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

632 
options [document = false] 
48481  633 
theories 
634 
ATP_Theory_Export 

635 
MaSh_Eval 

636 
MaSh_Export 

637 
TPTP_Interpret 

638 
THF_Arith 

639 
theories [proofs = 0] (* FIXME !? *) 

640 
ATP_Problem_Import 

641 

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

642 
session "HOLMultivariate_Analysis" (main) in Multivariate_Analysis = HOL + 
48481  643 
options [document_graph] 
644 
theories 

645 
Multivariate_Analysis 

646 
Determinants 

647 
files 

648 
"document/root.tex" 

649 

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

650 
session "HOLProbability" in "Probability" = "HOLMultivariate_Analysis" + 
48617  651 
options [document_graph] 
48481  652 
theories [document = false] 
653 
"~~/src/HOL/Library/Countable" 

654 
"~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits" 

655 
"~~/src/HOL/Library/Permutation" 

656 
theories 

657 
Probability 

658 
"ex/Dining_Cryptographers" 

659 
"ex/Koepf_Duermuth_Countermeasure" 

660 
files "document/root.tex" 

661 

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

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

663 
options [document = false] 
48481  664 
theories Nominal 
665 

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

666 
session "HOLNominalExamples" in "Nominal/Examples" = "HOLNominal" + 
48679  667 
options [timeout = 3600, condition = ISABELLE_POLYML, document = false] 
48481  668 
theories Nominal_Examples 
669 
theories [quick_and_dirty] VC_Condition 

670 

49310  671 
session "HOLCardinalsBase" in Cardinals = HOL + 
48978  672 
description {* Ordinals and Cardinals, Base Theories *} 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset

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

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

675 

49310  676 
session "HOLCardinals" in Cardinals = "HOLCardinalsBase" + 
48978  677 
description {* Ordinals and Cardinals, Full Theories *} 
49511
9f5bfef8bd82
created separate session "HOLBNFLFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents:
49510
diff
changeset

678 
options [document = false] 
49439  679 
theories Cardinals 
48984
f51d4a302962
do not hardwire document output options  to be provided by the user;
wenzelm
parents:
48978
diff
changeset

680 
files 
f51d4a302962
do not hardwire document output options  to be provided by the user;
wenzelm
parents:
48978
diff
changeset

681 
"document/intro.tex" 
f51d4a302962
do not hardwire document output options  to be provided by the user;
wenzelm
parents:
48978
diff
changeset

682 
"document/root.tex" 
f51d4a302962
do not hardwire document output options  to be provided by the user;
wenzelm
parents:
48978
diff
changeset

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

684 

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

685 
session "HOLBNFLFP" in BNF = "HOLCardinalsBase" + 
9f5bfef8bd82
created separate session "HOLBNFLFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents:
49510
diff
changeset

686 
description {* Bounded Natural Functors for Datatypes *} 
9f5bfef8bd82
created separate session "HOLBNFLFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents:
49510
diff
changeset

687 
options [document = false] 
9f5bfef8bd82
created separate session "HOLBNFLFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents:
49510
diff
changeset

688 
theories BNF_LFP 
9f5bfef8bd82
created separate session "HOLBNFLFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents:
49510
diff
changeset

689 

49517
c473c8749cd1
changed base session for "HOLBNF" for faster building in the typical case
blanchet
parents:
49511
diff
changeset

690 
session "HOLBNF" in BNF = "HOLCardinals" + 
49510
ba50d204095e
renamed "Codatatype" directory "BNF" (and corresponding session)  this opens the door to nononsense session names like "HOLBNFLFP"
blanchet
parents:
49483
diff
changeset

691 
description {* Bounded Natural Functors for (Co)datatypes *} 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset

692 
options [document = false] 
49510
ba50d204095e
renamed "Codatatype" directory "BNF" (and corresponding session)  this opens the door to nononsense session names like "HOLBNFLFP"
blanchet
parents:
49483
diff
changeset

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

694 

49510
ba50d204095e
renamed "Codatatype" directory "BNF" (and corresponding session)  this opens the door to nononsense session names like "HOLBNFLFP"
blanchet
parents:
49483
diff
changeset

695 
session "HOLBNFExamples" in "BNF/Examples" = "HOLBNF" + 
ba50d204095e
renamed "Codatatype" directory "BNF" (and corresponding session)  this opens the door to nononsense session names like "HOLBNFLFP"
blanchet
parents:
49483
diff
changeset

696 
description {* Examples for Bounded Natural Functors *} 
49932
9d3bc26485eb
back to parallel HOLBNFExamples, which seems to have suffered from Future.map on canceled persistent futures;
wenzelm
parents:
49903
diff
changeset

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

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

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

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

701 
TreeFsetI 
49872  702 
"Derivation_Trees/Gram_Lang" 
703 
"Derivation_Trees/Parallel" 

50517  704 
Koenig 
49693
393d7242adaf
thread the right local theory through + reenable parallel proofs for previously problematic theories
blanchet
parents:
49601
diff
changeset

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

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

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

708 

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

709 
session "HOLWord" (main) in Word = HOL + 
48481  710 
options [document_graph] 
711 
theories Word 

712 
files "document/root.bib" "document/root.tex" 

713 

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

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

715 
options [document = false] 
48481  716 
theories WordExamples 
717 

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

718 
session "HOLStatespace" in Statespace = HOL + 
48481  719 
theories StateSpaceEx 
720 
files "document/root.tex" 

721 

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

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

723 
description {* Nonstandard analysis. *} 
48481  724 
options [document_graph] 
725 
theories Hypercomplex 

726 
files "document/root.tex" 

727 

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

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

729 
options [document = false] 
48481  730 
theories NSPrimes 
731 

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

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

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

735 

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

736 
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

737 
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

738 
theories Ex 
48481  739 

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

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

741 
options [document = false, quick_and_dirty] 
48481  742 
theories 
743 
SMT_Examples 

744 
SMT_Word_Examples 

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

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

746 
SMT_Tests 
48481  747 
files 
748 
"SMT_Examples.certs" 

50665  749 
"SMT_Word_Examples.certs" 
48481  750 

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

751 
session "HOLBoogie" in "Boogie" = "HOLWord" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

752 
options [document = false] 
48481  753 
theories Boogie 
754 

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

755 
session "HOLBoogieExamples" in "Boogie/Examples" = "HOLBoogie" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

756 
options [document = false] 
48481  757 
theories 
758 
Boogie_Max_Stepwise 

759 
Boogie_Max 

760 
Boogie_Dijkstra 

761 
VCC_Max 

762 
files 

48493  763 
"Boogie_Dijkstra.b2i" 
48481  764 
"Boogie_Dijkstra.certs" 
48493  765 
"Boogie_Max.b2i" 
48481  766 
"Boogie_Max.certs" 
48493  767 
"VCC_Max.b2i" 
48481  768 
"VCC_Max.certs" 
769 

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

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

771 
options [document = false] 
48481  772 
theories SPARK 
773 

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

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

775 
options [document = false] 
48481  776 
theories 
777 
"Gcd/Greatest_Common_Divisor" 

778 

779 
"Liseq/Longest_Increasing_Subsequence" 

780 

781 
"RIPEMD160/F" 

782 
"RIPEMD160/Hash" 

783 
"RIPEMD160/K_L" 

784 
"RIPEMD160/K_R" 

785 
"RIPEMD160/R_L" 

786 
"RIPEMD160/Round" 

787 
"RIPEMD160/R_R" 

788 
"RIPEMD160/S_L" 

789 
"RIPEMD160/S_R" 

790 

791 
"Sqrt/Sqrt" 

792 
files 

793 
"Gcd/greatest_common_divisor/g_c_d.fdl" 

794 
"Gcd/greatest_common_divisor/g_c_d.rls" 

795 
"Gcd/greatest_common_divisor/g_c_d.siv" 

796 
"Liseq/liseq/liseq_length.fdl" 

797 
"Liseq/liseq/liseq_length.rls" 

798 
"Liseq/liseq/liseq_length.siv" 

799 
"RIPEMD160/rmd/f.fdl" 

800 
"RIPEMD160/rmd/f.rls" 

801 
"RIPEMD160/rmd/f.siv" 

802 
"RIPEMD160/rmd/hash.fdl" 

803 
"RIPEMD160/rmd/hash.rls" 

804 
"RIPEMD160/rmd/hash.siv" 

805 
"RIPEMD160/rmd/k_l.fdl" 

806 
"RIPEMD160/rmd/k_l.rls" 

807 
"RIPEMD160/rmd/k_l.siv" 

808 
"RIPEMD160/rmd/k_r.fdl" 

809 
"RIPEMD160/rmd/k_r.rls" 

810 
"RIPEMD160/rmd/k_r.siv" 

811 
"RIPEMD160/rmd/r_l.fdl" 

812 
"RIPEMD160/rmd/r_l.rls" 

813 
"RIPEMD160/rmd/r_l.siv" 

814 
"RIPEMD160/rmd/round.fdl" 

815 
"RIPEMD160/rmd/round.rls" 

816 
"RIPEMD160/rmd/round.siv" 

817 
"RIPEMD160/rmd/r_r.fdl" 

818 
"RIPEMD160/rmd/r_r.rls" 

819 
"RIPEMD160/rmd/r_r.siv" 

820 
"RIPEMD160/rmd/s_l.fdl" 

821 
"RIPEMD160/rmd/s_l.rls" 

822 
"RIPEMD160/rmd/s_l.siv" 

823 
"RIPEMD160/rmd/s_r.fdl" 

824 
"RIPEMD160/rmd/s_r.rls" 

825 
"RIPEMD160/rmd/s_r.siv" 

826 

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

827 
session "HOLSPARKManual" in "SPARK/Manual" = "HOLSPARK" + 
48486  828 
options [show_question_marks = false] 
48481  829 
theories 
830 
Example_Verification 

831 
VC_Principles 

832 
Reference 

833 
Complex_Types 

834 
files 

835 
"complex_types_app/initialize.fdl" 

836 
"complex_types_app/initialize.rls" 

837 
"complex_types_app/initialize.siv" 

838 
"document/complex_types.ads" 

839 
"document/complex_types_app.adb" 

840 
"document/complex_types_app.ads" 

841 
"document/Gcd.adb" 

842 
"document/Gcd.ads" 

843 
"document/intro.tex" 

844 
"document/loop_invariant.adb" 

845 
"document/loop_invariant.ads" 

846 
"document/root.bib" 

847 
"document/root.tex" 

848 
"document/Simple_Gcd.adb" 

849 
"document/Simple_Gcd.ads" 

850 
"loop_invariant/proc1.fdl" 

851 
"loop_invariant/proc1.rls" 

852 
"loop_invariant/proc1.siv" 

853 
"loop_invariant/proc2.fdl" 

854 
"loop_invariant/proc2.rls" 

855 
"loop_invariant/proc2.siv" 

856 
"simple_greatest_common_divisor/g_c_d.fdl" 

857 
"simple_greatest_common_divisor/g_c_d.rls" 

858 
"simple_greatest_common_divisor/g_c_d.siv" 

859 

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

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

861 
options [document = false] 
48481  862 
theories MutabelleExtra 
863 

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

864 
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

865 
options [document = false] 
48588  866 
theories 
48690  867 
Quickcheck_Examples 
868 
(* FIXME 

869 
Quickcheck_Lattice_Examples 

870 
Completeness 

871 
Quickcheck_Interfaces 

872 
Hotel_Example *) 

48598  873 
theories [condition = ISABELLE_GHC] 
874 
Quickcheck_Narrowing_Examples 

48588  875 

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

876 
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

877 
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

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

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

880 
Needham_Schroeder_Guided_Attacker_Example 
48690  881 
Needham_Schroeder_Unguided_Attacker_Example 
48481  882 

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

883 
session "HOLQuotient_Examples" in Quotient_Examples = HOL + 
48481  884 
description {* 
885 
Author: Cezary Kaliszyk and Christian Urban 

886 
*} 

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

887 
options [document = false] 
48481  888 
theories 
889 
DList 

890 
FSet 

891 
Quotient_Int 

892 
Quotient_Message 

893 
Lift_FSet 

894 
Lift_Set 

895 
Lift_Fun 

896 
Quotient_Rat 

897 
Lift_DList 

898 

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

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

900 
options [document = false] 
48690  901 
theories 
48481  902 
Examples 
903 
Predicate_Compile_Tests 

48690  904 
(* FIXME 
905 
Predicate_Compile_Quickcheck_Examples  should be added again soon (since 21Oct2010) *) 

48481  906 
Specialisation_Examples 
48690  907 
(* FIXME since 21Jul2011 
908 
Hotel_Example_Small_Generator 

909 
IMP_1 

910 
IMP_2 

911 
IMP_3 

912 
IMP_4 *) 

913 
theories [condition = "ISABELLE_SWIPL"] (* FIXME: *or* ISABELLE_YAP (??) *) 

914 
Code_Prolog_Examples 

915 
Context_Free_Grammar_Example 

916 
Hotel_Example_Prolog 

917 
Lambda_Example 

918 
List_Examples 

919 
theories [condition = "ISABELLE_SWIPL", quick_and_dirty] (* FIXME: *or* ISABELLE_YAP (??) *) 

920 
Reg_Exp_Example 

48481  921 

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

922 
session HOLCF (main) in HOLCF = HOL + 
48338  923 
description {* 
924 
Author: Franz Regensburger 

925 
Author: Brian Huffman 

926 

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

928 
*} 

929 
options [document_graph] 

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

930 
theories [document = false] 
48338  931 
"~~/src/HOL/Library/Nat_Bijection" 
932 
"~~/src/HOL/Library/Countable" 

48481  933 
theories 
934 
Plain_HOLCF 

935 
Fixrec 

936 
HOLCF 

937 
files "document/root.tex" 

938 

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

939 
session "HOLCFTutorial" in "HOLCF/Tutorial" = HOLCF + 
48481  940 
theories 
941 
Domain_ex 

942 
Fixrec_ex 

943 
New_Domain 

944 
files "document/root.tex" 

945 

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

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

947 
options [document = false] 
48481  948 
theories HOLCF_Library 
949 

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

950 
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

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

952 
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

953 

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

954 
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

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

956 
options [document = false] 
48481  957 
theories HoareEx 
48338  958 
files "document/root.tex" 
959 

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

960 
session "HOLCFex" in "HOLCF/ex" = HOLCF + 
48481  961 
description {* Misc HOLCF examples *} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

962 
options [document = false] 
48481  963 
theories 
964 
Dnat 

965 
Dagstuhl 

966 
Focus_ex 

967 
Fix2 

968 
Hoare 

969 
Concurrency_Monad 

970 
Loop 

971 
Powerdomain_ex 

972 
Domain_Proofs 

973 
Letrec 

974 
Pattern_Match 

975 

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

976 
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

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

978 
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

979 

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

980 
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

981 

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

982 
"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

983 
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

984 

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

985 
"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

986 
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

987 

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

988 
"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

989 
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

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

991 
options [document = false] 
48481  992 
theories 
993 
Fstreams 

994 
FOCUS 

995 
Buffer_adm 

996 

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

997 
session IOA in "HOLCF/IOA" = HOLCF + 
48481  998 
description {* 
999 
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

1000 
Copyright 1997 TU München 
48481  1001 

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

1002 
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

1003 

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

1004 
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

1005 
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

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

1008 
options [document = false] 
48481  1009 
theories "meta_theory/Abstraction" 
1010 

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

1011 
session "IOAABP" in "HOLCF/IOA/ABP" = IOA + 
48481  1012 
description {* 
1013 
Author: Olaf Mueller 

1014 

1015 
The Alternating Bit Protocol performed in I/OAutomata. 

1016 
*} 

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

1017 
options [document = false] 
48481  1018 
theories Correctness 
1019 

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

1020 
session "IOANTP" in "HOLCF/IOA/NTP" = IOA + 
48481  1021 
description {* 
1022 
Author: Tobias Nipkow & Konrad Slind 

1023 

1024 
A network transmission protocol, performed in the 

1025 
I/O automata formalization by Olaf Mueller. 

1026 
*} 

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

1027 
options [document = false] 
48481  1028 
theories Correctness 
1029 

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

1030 
session "IOAStorage" in "HOLCF/IOA/Storage" = IOA + 
48481  1031 
description {* 
1032 
Author: Olaf Mueller 

1033 

1034 
Memory storage case study. 

1035 
*} 

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

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

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

1039 
session "IOAex" in "HOLCF/IOA/ex" = IOA + 
48481  1040 
description {* 
1041 
Author: Olaf Mueller 

1042 
*} 

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

1043 
options [document = false] 
48481  1044 
theories 
1045 
TrivEx 

1046 
TrivEx2 

1047 

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

1048 
session "HOLDatatype_Benchmark" in Datatype_Benchmark = HOL + 
48481  1049 
description {* Some rather large datatype examples (from John Harrison). *} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

1050 
options [document = false] 
48635  1051 
theories [condition = ISABELLE_FULL_TEST, timing] 
48481  1052 
Brackin 
1053 
Instructions 

1054 
SML 

1055 
Verilog 

1056 

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

1057 
session "HOLRecord_Benchmark" in Record_Benchmark = HOL + 
48481  1058 
description {* Some benchmark on large record. *} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

1059 
options [document = false] 
48635  1060 
theories [condition = ISABELLE_FULL_TEST, timing] 
48481  1061 
Record_Benchmark 
1062 