author  nipkow 
Sat, 11 Aug 2012 11:31:05 +0200  
changeset 48765  fb1ed5230abc 
parent 48738  f8c1a5b9488f 
child 48901  5e0455e29339 
permissions  rwrr 
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset

1 
session HOL (main) = Pure + 
48338  2 
description {* Classical Higherorder Logic *} 
3 
options [document_graph] 

4 
theories Complex_Main 

48481  5 
files "document/root.bib" "document/root.tex" 
48338  6 

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

7 
session "HOLBase" = Pure + 
48338  8 
description {* Raw HOL base, with minimal tools *} 
48470
7483aa690b4f
clarified "document" again, eliminated redundant "no_document";
wenzelm
parents:
48458
diff
changeset

9 
options [document = false] 
48338  10 
theories HOL 
11 

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

12 
session "HOLPlain" = Pure + 
48338  13 
description {* HOL sideentry after bootstrap of many tools and packages *} 
48470
7483aa690b4f
clarified "document" again, eliminated redundant "no_document";
wenzelm
parents:
48458
diff
changeset

14 
options [document = false] 
48338  15 
theories Plain 
16 

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

17 
session "HOLMain" = Pure + 
48338  18 
description {* HOL sideentry for Main only, without Complex_Main *} 
48470
7483aa690b4f
clarified "document" again, eliminated redundant "no_document";
wenzelm
parents:
48458
diff
changeset

19 
options [document = false] 
48338  20 
theories Main 
21 

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

22 
session "HOLProofs" = Pure + 
48509  23 
description {* HOLMain with explicit proof terms *} 
48470
7483aa690b4f
clarified "document" again, eliminated redundant "no_document";
wenzelm
parents:
48458
diff
changeset

24 
options [document = false, proofs = 2, parallel_proofs = 0] 
48338  25 
theories Main 
26 

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

27 
session "HOLLibrary" in Library = HOL + 
48481  28 
description {* Classical Higherorder Logic  batteries included *} 
29 
theories 

30 
Library 

31 
List_Prefix 

32 
List_lexord 

33 
Sublist_Order 

34 
Product_Lattice 

35 
Code_Char_chr 

36 
Code_Char_ord 

37 
Code_Integer 

38 
Efficient_Nat 

48721  39 
(* Code_Prolog FIXME cf. 76965c356d2a *) 
48481  40 
Code_Real_Approx_By_Float 
41 
Target_Numeral 

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

43 

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

44 
session "HOLHahn_Banach" in Hahn_Banach = HOL + 
48481  45 
description {* 
46 
Author: Gertrud Bauer, TU Munich 

47 

48 
The HahnBanach theorem for real vector spaces. 

49 
*} 

50 
options [document_graph] 

51 
theories Hahn_Banach 

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

53 

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

54 
session "HOLInduct" in Induct = HOL + 
48481  55 
theories [quick_and_dirty] 
56 
Common_Patterns 

57 
theories 

58 
QuoDataType 

59 
QuoNestedDataType 

60 
Term 

61 
SList 

62 
ABexp 

63 
Tree 

64 
Ordinals 

65 
Sigma_Algebra 

66 
Comb 

67 
PropLog 

68 
Com 

69 
files "document/root.tex" 

70 

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

71 
session "HOLIMP" in IMP = HOL + 
48481  72 
options [document_graph] 
73 
theories [document = false] 

74 
"~~/src/HOL/ex/Interpretation_with_Defs" 

75 
"~~/src/HOL/Library/While_Combinator" 

76 
"~~/src/HOL/Library/Char_ord" 

77 
"~~/src/HOL/Library/List_lexord" 

78 
theories 

79 
BExp 

80 
ASM 

81 
Small_Step 

82 
Denotation 

83 
Comp_Rev 

84 
Poly_Types 

85 
Sec_Typing 

86 
Sec_TypingT 

87 
Def_Ass_Sound_Big 

88 
Def_Ass_Sound_Small 

89 
Live 

90 
Live_True 

91 
Hoare_Examples 

92 
VC 

93 
HoareT 

94 
Collecting1 

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

95 
Collecting_Examples 
48481  96 
Abs_Int_Tests 
97 
Abs_Int1_parity 

98 
Abs_Int1_const 

99 
Abs_Int3 

100 
"Abs_Int_ITP/Abs_Int1_parity_ITP" 

101 
"Abs_Int_ITP/Abs_Int1_const_ITP" 

102 
"Abs_Int_ITP/Abs_Int3_ITP" 

103 
"Abs_Int_Den/Abs_Int_den2" 

104 
Procs_Dyn_Vars_Dyn 

105 
Procs_Stat_Vars_Dyn 

106 
Procs_Stat_Vars_Stat 

107 
C_like 

108 
OO 

109 
Fold 

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

111 

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

112 
session "HOLIMPP" in IMPP = HOL + 
48481  113 
description {* 
114 
Author: David von Oheimb 

115 
Copyright 1999 TUM 

116 
*} 

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

117 
options [document = false] 
48481  118 
theories EvenOdd 
119 

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

120 
session "HOLImport" in Import = HOL + 
48481  121 
options [document_graph] 
122 
theories HOL_Light_Maps 

123 
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 

124 

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

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

126 
options [document = false] 
48481  127 
theories Number_Theory 
128 

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

129 
session "HOLOld_Number_Theory" in Old_Number_Theory = HOL + 
48481  130 
options [document_graph] 
131 
theories [document = false] 

132 
"~~/src/HOL/Library/Infinite_Set" 

133 
"~~/src/HOL/Library/Permutation" 

134 
theories 

135 
Fib 

136 
Factorization 

137 
Chinese 

138 
WilsonRuss 

139 
WilsonBij 

140 
Quadratic_Reciprocity 

141 
Primes 

142 
Pocklington 

143 
files "document/root.tex" 

144 

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

145 
session "HOLHoare" in Hoare = HOL + 
48481  146 
theories Hoare 
147 
files "document/root.bib" "document/root.tex" 

148 

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

149 
session "HOLHoare_Parallel" in Hoare_Parallel = HOL + 
48481  150 
options [document_graph] 
151 
theories Hoare_Parallel 

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

153 

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

154 
session "HOLCodegenerator_Test" in Codegenerator_Test = "HOLLibrary" + 
48481  155 
options [document = false, document_graph = false, browser_info = false] 
48624  156 
theories Generate Generate_Pretty RBT_Set_Test 
48481  157 

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

158 
session "HOLMetis_Examples" in Metis_Examples = HOL + 
48481  159 
description {* 
160 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

161 
Author: Jasmin Blanchette, TU Muenchen 

162 

163 
Testing Metis and Sledgehammer. 

164 
*} 

48679  165 
options [timeout = 3600, document = false] 
48481  166 
theories 
167 
Abstraction 

168 
Big_O 

169 
Binary_Tree 

170 
Clausification 

171 
Message 

172 
Proxies 

173 
Tarski 

174 
Trans_Closure 

175 
Sets 

176 

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

177 
session "HOLNitpick_Examples" in Nitpick_Examples = HOL + 
48481  178 
description {* 
179 
Author: Jasmin Blanchette, TU Muenchen 

180 
Copyright 2009 

181 
*} 

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

182 
options [document = false] 
48481  183 
theories [quick_and_dirty] Nitpick_Examples 
184 

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

185 
session "HOLAlgebra" in Algebra = HOL + 
48481  186 
description {* 
187 
Author: Clemens Ballarin, started 24 September 1999 

188 

189 
The Isabelle Algebraic Library. 

190 
*} 

191 
options [document_graph] 

192 
theories [document = false] 

193 
(* Preliminaries from set and number theory *) 

194 
"~~/src/HOL/Library/FuncSet" 

195 
"~~/src/HOL/Old_Number_Theory/Primes" 

196 
"~~/src/HOL/Library/Binomial" 

197 
"~~/src/HOL/Library/Permutation" 

198 
theories 

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

200 
(* Groups *) 

201 
FiniteProduct (* Product operator for commutative groups *) 

202 
Sylow (* Sylow's theorem *) 

203 
Bij (* Automorphism Groups *) 

204 

205 
(* Rings *) 

206 
Divisibility (* Rings *) 

207 
IntRing (* Ideals and residue classes *) 

208 
UnivPoly (* Polynomials *) 

209 
theories [document = false] 

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

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

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

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

214 

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

215 
session "HOLAuth" in Auth = HOL + 
48481  216 
options [document_graph] 
217 
theories 

218 
Auth_Shared 

219 
Auth_Public 

220 
"Smartcard/Auth_Smartcard" 

221 
"Guard/Auth_Guard_Shared" 

222 
"Guard/Auth_Guard_Public" 

223 
files "document/root.tex" 

224 

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

225 
session "HOLUNITY" in UNITY = HOL + 
48481  226 
description {* 
227 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

228 
Copyright 1998 University of Cambridge 

229 

230 
Verifying security protocols using UNITY. 

231 
*} 

232 
options [document_graph] 

233 
theories [document = false] "../Auth/Public" 

234 
theories 

235 
(*Basic metatheory*) 

236 
"UNITY_Main" 

237 

238 
(*Simple examples: no composition*) 

239 
"Simple/Deadlock" 

240 
"Simple/Common" 

241 
"Simple/Network" 

242 
"Simple/Token" 

243 
"Simple/Channel" 

244 
"Simple/Lift" 

245 
"Simple/Mutex" 

246 
"Simple/Reach" 

247 
"Simple/Reachability" 

248 

249 
(*Verifying security protocols using UNITY*) 

250 
"Simple/NSP_Bad" 

251 

252 
(*Example of composition*) 

253 
"Comp/Handshake" 

254 

255 
(*Universal properties examples*) 

256 
"Comp/Counter" 

257 
"Comp/Counterc" 

258 
"Comp/Priority" 

259 

260 
"Comp/TimerArray" 

261 
"Comp/Progress" 

262 

263 
"Comp/Alloc" 

264 
"Comp/AllocImpl" 

265 
"Comp/Client" 

266 

267 
(*obsolete*) 

268 
"ELT" 

269 
files "document/root.tex" 

270 

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

271 
session "HOLUnix" in Unix = HOL + 
48481  272 
options [print_mode = "no_brackets,no_type_brackets"] 
273 
theories Unix 

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

275 

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

276 
session "HOLZF" in ZF = HOL + 
48481  277 
description {* *} 
278 
theories MainZF Games 

279 
files "document/root.tex" 

280 

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

281 
session "HOLImperative_HOL" in Imperative_HOL = HOL + 
48481  282 
description {* *} 
283 
options [document_graph, print_mode = "iff,no_brackets"] 

284 
theories [document = false] 

285 
"~~/src/HOL/Library/Countable" 

286 
"~~/src/HOL/Library/Monad_Syntax" 

287 
"~~/src/HOL/Library/Code_Natural" 

288 
"~~/src/HOL/Library/LaTeXsugar" 

289 
theories Imperative_HOL_ex 

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

291 

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

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

293 
options [condition = ISABELLE_POLYML, document = false] 
48481  294 
theories Decision_Procs 
295 

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

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

297 
options [document = false, proofs = 2, parallel_proofs = 0] 
48481  298 
theories Hilbert_Classical 
299 

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

300 
session "HOLProofsExtraction" in "Proofs/Extraction" = "HOLProofs" + 
48481  301 
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

302 
options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0] 
48481  303 
theories [document = false] 
304 
"~~/src/HOL/Library/Efficient_Nat" 

305 
"~~/src/HOL/Library/Monad_Syntax" 

306 
"~~/src/HOL/Number_Theory/Primes" 

307 
"~~/src/HOL/Number_Theory/UniqueFactorization" 

308 
"~~/src/HOL/Library/State_Monad" 

309 
theories 

310 
Greatest_Common_Divisor 

311 
Warshall 

312 
Higman_Extraction 

313 
Pigeonhole 

314 
Euclid 

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

316 

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

317 
session "HOLProofsLambda" in "Proofs/Lambda" = "HOLProofs" + 
48481  318 
options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0] 
319 
theories [document = false] 

320 
"~~/src/HOL/Library/Code_Integer" 

321 
theories 

322 
Eta 

323 
StrongNorm 

324 
Standardization 

325 
WeakNorm 

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

327 

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

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

331 
*} 

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

332 
options [document = false] 
48481  333 
theories Test Type 
334 

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

335 
session "HOLMicroJava" in MicroJava = HOL + 
48481  336 
options [document_graph] 
337 
theories [document = false] "~~/src/HOL/Library/While_Combinator" 

338 
theories MicroJava 

339 
files 

340 
"document/introduction.tex" 

341 
"document/root.bib" 

342 
"document/root.tex" 

343 

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

344 
session "HOLMicroJavaskip_proofs" in MicroJava = HOL + 
48636  345 
options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs, quick_and_dirty] 
346 
theories MicroJava 

347 

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

348 
session "HOLNanoJava" in NanoJava = HOL + 
48481  349 
options [document_graph] 
350 
theories Example 

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

352 

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

353 
session "HOLBali" in Bali = HOL + 
48481  354 
options [document_graph] 
355 
theories 

356 
AxExample 

357 
AxSound 

358 
AxCompl 

359 
Trans 

360 
files "document/root.tex" 

361 

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

362 
session "HOLIOA" in IOA = HOL + 
48481  363 
description {* 
364 
Author: Tobias Nipkow & Konrad Slind 

365 
Copyright 1994 TU Muenchen 

366 

367 
The meta theory of I/OAutomata. 

368 

369 
@inproceedings{NipkowSlindIOA, 

370 
author={Tobias Nipkow and Konrad Slind}, 

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

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

373 
publisher=Springer, 

374 
series=LNCS, 

375 
note={To appear}} 

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

377 

378 
and 

379 

380 
@inproceedings{MuellerNipkow, 

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

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

383 
booktitle={Proc.\ TACAS Workshop}, 

384 
organization={Aarhus University, BRICS report}, 

385 
year=1995} 

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

387 
*} 

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

388 
options [document = false] 
48481  389 
theories Solve 
390 

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

391 
session "HOLLattice" in Lattice = HOL + 
48481  392 
description {* 
393 
Author: Markus Wenzel, TU Muenchen 

394 

395 
Basic theory of lattices and orders. 

396 
*} 

397 
theories CompleteLattice 

398 
files "document/root.tex" 

399 

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

400 
session "HOLex" in ex = HOL + 
48481  401 
description {* Miscellaneous examples for HigherOrder Logic. *} 
48679  402 
options [timeout = 3600, condition = ISABELLE_POLYML] 
48481  403 
theories [document = false] 
404 
"~~/src/HOL/Library/State_Monad" 

405 
Code_Nat_examples 

406 
"~~/src/HOL/Library/FuncSet" 

407 
Eval_Examples 

408 
Normalization_by_Evaluation 

409 
Hebrew 

410 
Chinese 

411 
Serbian 

412 
"~~/src/HOL/Library/FinFun_Syntax" 

413 
theories 

414 
Iff_Oracle 

415 
Coercion_Examples 

416 
Numeral_Representation 

417 
Higher_Order_Logic 

418 
Abstract_NAT 

419 
Guess 

420 
Binary 

421 
Fundefs 

422 
Induction_Schema 

423 
LocaleTest2 

424 
Records 

425 
While_Combinator_Example 

426 
MonoidGroup 

427 
BinEx 

428 
Hex_Bin_Examples 

429 
Antiquote 

430 
Multiquote 

431 
PER 

432 
NatSum 

433 
ThreeDivides 

434 
Intuitionistic 

435 
CTL 

436 
Arith_Examples 

437 
BT 

438 
Tree23 

439 
MergeSort 

440 
Lagrange 

441 
Groebner_Examples 

442 
MT 

443 
Unification 

444 
Primrec 

445 
Tarski 

446 
Classical 

447 
Set_Theory 

448 
Meson_Test 

449 
Termination 

450 
Coherent 

451 
PresburgerEx 

452 
ReflectionEx 

453 
Sqrt 

454 
Sqrt_Script 

455 
Transfer_Ex 

456 
Transfer_Int_Nat 

457 
HarmonicSeries 

458 
Refute_Examples 

459 
Landau 

460 
Execute_Choice 

461 
Summation 

462 
Gauge_Integration 

463 
Dedekind_Real 

464 
Quicksort 

465 
Birthday_Paradox 

466 
List_to_Set_Comprehension_Examples 

467 
Seq 

468 
Simproc_Tests 

469 
Executable_Relation 

470 
FinFunPred 

471 
Set_Comprehension_Pointfree_Tests 

472 
Parallel_Example 

473 
theories SVC_Oracle 

48690  474 
theories [condition = SVC_HOME] 
475 
svc_test 

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

478 
Sudoku 

479 
(* FIXME 

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

481 
(*global sideeffects ahead!*) 

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

483 
*) 

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

485 

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

486 
session "HOLIsar_Examples" in Isar_Examples = HOL + 
48481  487 
description {* Miscellaneous Isabelle/Isar examples for HigherOrder Logic. *} 
488 
theories [document = false] 

489 
"~~/src/HOL/Library/Lattice_Syntax" 

490 
"../Number_Theory/Primes" 

491 
theories 

492 
Basic_Logic 

493 
Cantor 

494 
Drinker 

495 
Expr_Compiler 

496 
Fibonacci 

497 
Group 

498 
Group_Context 

499 
Group_Notepad 

500 
Hoare_Ex 

501 
Knaster_Tarski 

502 
Mutilated_Checkerboard 

503 
Nested_Datatype 

504 
Peirce 

505 
Puzzle 

506 
Summation 

507 
files 

508 
"document/root.bib" 

509 
"document/root.tex" 

510 
"document/style.tex" 

511 

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

512 
session "HOLSET_Protocol" in SET_Protocol = HOL + 
48481  513 
options [document_graph] 
514 
theories [document = false] "~~/src/HOL/Library/Nat_Bijection" 

515 
theories SET_Protocol 

516 
files "document/root.tex" 

517 

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

518 
session "HOLMatrix_LP" in Matrix_LP = HOL + 
48481  519 
options [document_graph] 
520 
theories Cplex 

521 
files "document/root.tex" 

522 

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

523 
session "HOLTLA" in TLA = HOL + 
48481  524 
description {* The Temporal Logic of Actions *} 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

525 
options [document = false] 
48481  526 
theories TLA 
527 

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

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

529 
options [document = false] 
48481  530 
theories Inc 
531 

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

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

533 
options [document = false] 
48481  534 
theories DBuffer 
535 

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

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

537 
options [document = false] 
48481  538 
theories MemoryImplementation 
539 

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

540 
session "HOLTPTP" in TPTP = HOL + 
48481  541 
description {* 
542 
Author: Jasmin Blanchette, TU Muenchen 

543 
Author: Nik Sultana, University of Cambridge 

544 
Copyright 2011 

545 

546 
TPTPrelated extensions. 

547 
*} 

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

548 
options [document = false] 
48481  549 
theories 
550 
ATP_Theory_Export 

551 
MaSh_Eval 

552 
MaSh_Export 

553 
TPTP_Interpret 

554 
THF_Arith 

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

556 
ATP_Problem_Import 

557 

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

558 
session "HOLMultivariate_Analysis" in Multivariate_Analysis = HOL + 
48481  559 
options [document_graph] 
560 
theories 

561 
Multivariate_Analysis 

562 
Determinants 

563 
files 

564 
"Integration.certs" 

565 
"document/root.tex" 

566 

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

567 
session "HOLProbability" in "Probability" = "HOLMultivariate_Analysis" + 
48617  568 
options [document_graph] 
48481  569 
theories [document = false] 
570 
"~~/src/HOL/Library/Countable" 

571 
"~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits" 

572 
"~~/src/HOL/Library/Permutation" 

573 
theories 

574 
Probability 

575 
"ex/Dining_Cryptographers" 

576 
"ex/Koepf_Duermuth_Countermeasure" 

577 
files "document/root.tex" 

578 

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

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

580 
options [document = false] 
48481  581 
theories Nominal 
582 

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

583 
session "HOLNominalExamples" in "Nominal/Examples" = "HOLNominal" + 
48679  584 
options [timeout = 3600, condition = ISABELLE_POLYML, document = false] 
48481  585 
theories Nominal_Examples 
586 
theories [quick_and_dirty] VC_Condition 

587 

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

588 
session "HOLWord" in Word = HOL + 
48481  589 
options [document_graph] 
590 
theories Word 

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

592 

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

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

594 
options [document = false] 
48481  595 
theories WordExamples 
596 

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

597 
session "HOLStatespace" in Statespace = HOL + 
48481  598 
theories StateSpaceEx 
599 
files "document/root.tex" 

600 

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

601 
session "HOLNSA" in NSA = HOL + 
48481  602 
options [document_graph] 
603 
theories Hypercomplex 

604 
files "document/root.tex" 

605 

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

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

607 
options [document = false] 
48481  608 
theories NSPrimes 
609 

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

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

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

613 

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

614 
session "HOLMirabelleex" in "Mirabelle/ex" = "HOLMirabelle" + 
48589
fb446a780d50
separate session HOLMirabelleex  cannot run isolated shell scripts within build tool;
wenzelm
parents:
48588
diff
changeset

615 
theories Ex 
48481  616 

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

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

618 
options [document = false, quick_and_dirty] 
48481  619 
theories 
620 
SMT_Tests 

621 
SMT_Examples 

622 
SMT_Word_Examples 

623 
files 

624 
"SMT_Examples.certs" 

625 
"SMT_Tests.certs" 

626 

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

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

628 
options [document = false] 
48481  629 
theories Boogie 
630 

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

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

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

635 
Boogie_Max 

636 
Boogie_Dijkstra 

637 
VCC_Max 

638 
files 

48493  639 
"Boogie_Dijkstra.b2i" 
48481  640 
"Boogie_Dijkstra.certs" 
48493  641 
"Boogie_Max.b2i" 
48481  642 
"Boogie_Max.certs" 
48493  643 
"VCC_Max.b2i" 
48481  644 
"VCC_Max.certs" 
645 

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

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

647 
options [document = false] 
48481  648 
theories SPARK 
649 

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

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

651 
options [document = false] 
48481  652 
theories 
653 
"Gcd/Greatest_Common_Divisor" 

654 

655 
"Liseq/Longest_Increasing_Subsequence" 

656 

657 
"RIPEMD160/F" 

658 
"RIPEMD160/Hash" 

659 
"RIPEMD160/K_L" 

660 
"RIPEMD160/K_R" 

661 
"RIPEMD160/R_L" 

662 
"RIPEMD160/Round" 

663 
"RIPEMD160/R_R" 

664 
"RIPEMD160/S_L" 

665 
"RIPEMD160/S_R" 

666 

667 
"Sqrt/Sqrt" 

668 
files 

669 
"Gcd/greatest_common_divisor/g_c_d.fdl" 

670 
"Gcd/greatest_common_divisor/g_c_d.rls" 

671 
"Gcd/greatest_common_divisor/g_c_d.siv" 

672 
"Liseq/liseq/liseq_length.fdl" 

673 
"Liseq/liseq/liseq_length.rls" 

674 
"Liseq/liseq/liseq_length.siv" 

675 
"RIPEMD160/rmd/f.fdl" 

676 
"RIPEMD160/rmd/f.rls" 

677 
"RIPEMD160/rmd/f.siv" 

678 
"RIPEMD160/rmd/hash.fdl" 

679 
"RIPEMD160/rmd/hash.rls" 

680 
"RIPEMD160/rmd/hash.siv" 

681 
"RIPEMD160/rmd/k_l.fdl" 

682 
"RIPEMD160/rmd/k_l.rls" 

683 
"RIPEMD160/rmd/k_l.siv" 

684 
"RIPEMD160/rmd/k_r.fdl" 

685 
"RIPEMD160/rmd/k_r.rls" 

686 
"RIPEMD160/rmd/k_r.siv" 

687 
"RIPEMD160/rmd/r_l.fdl" 

688 
"RIPEMD160/rmd/r_l.rls" 

689 
"RIPEMD160/rmd/r_l.siv" 

690 
"RIPEMD160/rmd/round.fdl" 

691 
"RIPEMD160/rmd/round.rls" 

692 
"RIPEMD160/rmd/round.siv" 

693 
"RIPEMD160/rmd/r_r.fdl" 

694 
"RIPEMD160/rmd/r_r.rls" 

695 
"RIPEMD160/rmd/r_r.siv" 

696 
"RIPEMD160/rmd/s_l.fdl" 

697 
"RIPEMD160/rmd/s_l.rls" 

698 
"RIPEMD160/rmd/s_l.siv" 

699 
"RIPEMD160/rmd/s_r.fdl" 

700 
"RIPEMD160/rmd/s_r.rls" 

701 
"RIPEMD160/rmd/s_r.siv" 

702 

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

703 
session "HOLSPARKManual" in "SPARK/Manual" = "HOLSPARK" + 
48486  704 
options [show_question_marks = false] 
48481  705 
theories 
706 
Example_Verification 

707 
VC_Principles 

708 
Reference 

709 
Complex_Types 

710 
files 

711 
"complex_types_app/initialize.fdl" 

712 
"complex_types_app/initialize.rls" 

713 
"complex_types_app/initialize.siv" 

714 
"document/complex_types.ads" 

715 
"document/complex_types_app.adb" 

716 
"document/complex_types_app.ads" 

717 
"document/Gcd.adb" 

718 
"document/Gcd.ads" 

719 
"document/intro.tex" 

720 
"document/loop_invariant.adb" 

721 
"document/loop_invariant.ads" 

722 
"document/root.bib" 

723 
"document/root.tex" 

724 
"document/Simple_Gcd.adb" 

725 
"document/Simple_Gcd.ads" 

726 
"loop_invariant/proc1.fdl" 

727 
"loop_invariant/proc1.rls" 

728 
"loop_invariant/proc1.siv" 

729 
"loop_invariant/proc2.fdl" 

730 
"loop_invariant/proc2.rls" 

731 
"loop_invariant/proc2.siv" 

732 
"simple_greatest_common_divisor/g_c_d.fdl" 

733 
"simple_greatest_common_divisor/g_c_d.rls" 

734 
"simple_greatest_common_divisor/g_c_d.siv" 

735 

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

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

737 
options [document = false] 
48481  738 
theories MutabelleExtra 
739 

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

740 
session "HOLQuickcheck_Examples" in Quickcheck_Examples = HOL + 
48679  741 
options [timeout = 3600, document = false] 
48588  742 
theories 
48690  743 
Quickcheck_Examples 
744 
(* FIXME 

745 
Quickcheck_Lattice_Examples 

746 
Completeness 

747 
Quickcheck_Interfaces 

748 
Hotel_Example *) 

48598  749 
theories [condition = ISABELLE_GHC] 
750 
Quickcheck_Narrowing_Examples 

48588  751 

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

752 
session "HOLQuickcheck_Benchmark" in Quickcheck_Benchmark = HOL + 
48635  753 
theories [condition = ISABELLE_FULL_TEST, quick_and_dirty] 
48618
1f7e068b4613
moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents:
48614
diff
changeset

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

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

756 
Needham_Schroeder_Guided_Attacker_Example 
48690  757 
Needham_Schroeder_Unguided_Attacker_Example 
48481  758 

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

759 
session "HOLQuotient_Examples" in Quotient_Examples = HOL + 
48481  760 
description {* 
761 
Author: Cezary Kaliszyk and Christian Urban 

762 
*} 

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

763 
options [document = false] 
48481  764 
theories 
765 
DList 

766 
FSet 

767 
Quotient_Int 

768 
Quotient_Message 

769 
Lift_FSet 

770 
Lift_Set 

771 
Lift_Fun 

772 
Quotient_Rat 

773 
Lift_DList 

774 

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

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

776 
options [document = false] 
48690  777 
theories 
48481  778 
Examples 
779 
Predicate_Compile_Tests 

48690  780 
(* FIXME 
781 
Predicate_Compile_Quickcheck_Examples  should be added again soon (since 21Oct2010) *) 

48481  782 
Specialisation_Examples 
48690  783 
(* FIXME since 21Jul2011 
784 
Hotel_Example_Small_Generator 

785 
IMP_1 

786 
IMP_2 

787 
IMP_3 

788 
IMP_4 *) 

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

790 
Code_Prolog_Examples 

791 
Context_Free_Grammar_Example 

792 
Hotel_Example_Prolog 

793 
Lambda_Example 

794 
List_Examples 

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

796 
Reg_Exp_Example 

48481  797 

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

798 
session HOLCF (main) in HOLCF = HOL + 
48338  799 
description {* 
800 
Author: Franz Regensburger 

801 
Author: Brian Huffman 

802 

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

804 
*} 

805 
options [document_graph] 

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

806 
theories [document = false] 
48338  807 
"~~/src/HOL/Library/Nat_Bijection" 
808 
"~~/src/HOL/Library/Countable" 

48481  809 
theories 
810 
Plain_HOLCF 

811 
Fixrec 

812 
HOLCF 

813 
files "document/root.tex" 

814 

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

815 
session "HOLCFTutorial" in "HOLCF/Tutorial" = HOLCF + 
48481  816 
theories 
817 
Domain_ex 

818 
Fixrec_ex 

819 
New_Domain 

820 
files "document/root.tex" 

821 

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

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

823 
options [document = false] 
48481  824 
theories HOLCF_Library 
825 

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

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

827 
options [document = false] 
48481  828 
theories HoareEx 
48338  829 
files "document/root.tex" 
830 

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

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

833 
options [document = false] 
48481  834 
theories 
835 
Dnat 

836 
Dagstuhl 

837 
Focus_ex 

838 
Fix2 

839 
Hoare 

840 
Concurrency_Monad 

841 
Loop 

842 
Powerdomain_ex 

843 
Domain_Proofs 

844 
Letrec 

845 
Pattern_Match 

846 

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

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

848 
options [document = false] 
48481  849 
theories 
850 
Fstreams 

851 
FOCUS 

852 
Buffer_adm 

853 

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

854 
session IOA in "HOLCF/IOA" = HOLCF + 
48481  855 
description {* 
856 
Author: Olaf Mueller 

857 

858 
Formalization of a semantic model of I/OAutomata. 

859 
*} 

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

860 
options [document = false] 
48481  861 
theories "meta_theory/Abstraction" 
862 

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

863 
session "IOAABP" in "HOLCF/IOA/ABP" = IOA + 
48481  864 
description {* 
865 
Author: Olaf Mueller 

866 

867 
The Alternating Bit Protocol performed in I/OAutomata. 

868 
*} 

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

869 
options [document = false] 
48481  870 
theories Correctness 
871 

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

872 
session "IOANTP" in "HOLCF/IOA/NTP" = IOA + 
48481  873 
description {* 
874 
Author: Tobias Nipkow & Konrad Slind 

875 

876 
A network transmission protocol, performed in the 

877 
I/O automata formalization by Olaf Mueller. 

878 
*} 

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

879 
options [document = false] 
48481  880 
theories Correctness 
881 

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

882 
session "IOAStorage" in "HOLCF/IOA/Storage" = IOA + 
48481  883 
description {* 
884 
Author: Olaf Mueller 

885 

886 
Memory storage case study. 

887 
*} 

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

888 
options [document = false] 
48481  889 
theories Correctness 
890 

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

891 
session "IOAex" in "HOLCF/IOA/ex" = IOA + 
48481  892 
description {* 
893 
Author: Olaf Mueller 

894 
*} 

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

895 
options [document = false] 
48481  896 
theories 
897 
TrivEx 

898 
TrivEx2 

899 

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

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

902 
options [document = false] 
48635  903 
theories [condition = ISABELLE_FULL_TEST, timing] 
48481  904 
Brackin 
905 
Instructions 

906 
SML 

907 
Verilog 

908 

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

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

911 
options [document = false] 
48635  912 
theories [condition = ISABELLE_FULL_TEST, timing] 
48481  913 
Record_Benchmark 
914 