author  blanchet 
Tue, 08 Apr 2014 18:06:21 +0200  
changeset 56454  e9e82384e5a1 
parent 56215  fcf90317383d 
child 56676  015f9e5e4fae 
permissions  rwrr 
51397
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
51263
diff
changeset

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

2 

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

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

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

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

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

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

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

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

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

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

13 
"document/root.tex" 
48338  14 

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

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

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

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

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

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

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

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

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

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

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

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

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

29 
*} 
48481  30 
theories 
31 
Library 

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

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

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

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

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

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

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

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

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

41 
Code_Char 
55447  42 
Code_Prolog 
48481  43 
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

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

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

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

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

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

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

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

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

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

53 
Sum_of_Squares_Remote 
48481  54 
files "document/root.bib" "document/root.tex" 
55 

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

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

59 

60 
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

61 

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

62 
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

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

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

65 
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

66 

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

67 
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

68 
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

69 

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

70 
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

71 
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

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

75 
theories Hahn_Banach 

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

77 

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

78 
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

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

80 
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

81 

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

82 
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

83 
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

84 

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

85 
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

86 
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

87 

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

88 
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

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

90 
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

91 

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

92 
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

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

94 
*} 
48481  95 
theories [quick_and_dirty] 
96 
Common_Patterns 

97 
theories 

98 
QuoDataType 

99 
QuoNestedDataType 

100 
Term 

101 
SList 

102 
ABexp 

103 
Tree 

104 
Ordinals 

105 
Sigma_Algebra 

106 
Comb 

107 
PropLog 

108 
Com 

109 
files "document/root.tex" 

110 

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

111 
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

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

117 
"~~/src/HOL/Library/List_lexord" 

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

48481  120 
theories 
121 
BExp 

122 
ASM 

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

128 
Sec_TypingT 

52726  129 
Def_Init_Big 
130 
Def_Init_Small 

131 
Fold 

48481  132 
Live 
133 
Live_True 

134 
Hoare_Examples 

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

138 
Collecting_Examples 
48481  139 
Abs_Int_Tests 
140 
Abs_Int1_parity 

141 
Abs_Int1_const 

142 
Abs_Int3 

143 
"Abs_Int_ITP/Abs_Int1_parity_ITP" 

144 
"Abs_Int_ITP/Abs_Int1_const_ITP" 

145 
"Abs_Int_ITP/Abs_Int3_ITP" 

146 
"Abs_Int_Den/Abs_Int_den2" 

147 
Procs_Dyn_Vars_Dyn 

148 
Procs_Stat_Vars_Dyn 

149 
Procs_Stat_Vars_Stat 

150 
C_like 

151 
OO 

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 "HOLIMPP" in IMPP = HOL + 
48481  155 
description {* 
156 
Author: David von Oheimb 

157 
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

158 

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

159 
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

160 

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

161 
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

162 
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

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

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

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

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

171 
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 

172 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

187 
Number_Theory 
55370  188 
files 
189 
"document/root.tex" 

48481  190 

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

191 
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

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

193 
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

194 
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

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

198 
"~~/src/HOL/Library/Infinite_Set" 

199 
"~~/src/HOL/Library/Permutation" 

200 
theories 

201 
Fib 

202 
Factorization 

203 
Chinese 

204 
WilsonRuss 

205 
WilsonBij 

206 
Quadratic_Reciprocity 

207 
Primes 

208 
Pocklington 

209 
files "document/root.tex" 

210 

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

211 
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

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

213 
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

214 
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

215 
*} 
48481  216 
theories Hoare 
217 
files "document/root.bib" "document/root.tex" 

218 

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

219 
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

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

221 
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

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

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

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

227 

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

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

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

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

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

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

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

235 
Generate_Pretty_Char 
48481  236 

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

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

240 
Author: Jasmin Blanchette, TU Muenchen 

241 

242 
Testing Metis and Sledgehammer. 

243 
*} 

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

247 
Big_O 

248 
Binary_Tree 

249 
Clausification 

250 
Message 

251 
Proxies 

252 
Tarski 

253 
Trans_Closure 

254 
Sets 

255 

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

259 
Copyright 2009 

260 
*} 

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

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

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

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

267 

268 
The Isabelle Algebraic Library. 

269 
*} 

270 
options [document_graph] 

271 
theories [document = false] 

272 
(* Preliminaries from set and number theory *) 

273 
"~~/src/HOL/Library/FuncSet" 

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

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

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

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

279 
(* Groups *) 

280 
FiniteProduct (* Product operator for commutative groups *) 

281 
Sylow (* Sylow's theorem *) 

282 
Bij (* Automorphism Groups *) 

283 

284 
(* Rings *) 

285 
Divisibility (* Rings *) 

286 
IntRing (* Ideals and residue classes *) 

287 
UnivPoly (* Polynomials *) 

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

289 

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

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

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

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

293 
*} 
48481  294 
options [document_graph] 
295 
theories 

296 
Auth_Shared 

297 
Auth_Public 

298 
"Smartcard/Auth_Smartcard" 

299 
"Guard/Auth_Guard_Shared" 

300 
"Guard/Auth_Guard_Public" 

301 
files "document/root.tex" 

302 

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

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

306 
Copyright 1998 University of Cambridge 

307 

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

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

311 
theories 

312 
(*Basic metatheory*) 

313 
"UNITY_Main" 

314 

315 
(*Simple examples: no composition*) 

316 
"Simple/Deadlock" 

317 
"Simple/Common" 

318 
"Simple/Network" 

319 
"Simple/Token" 

320 
"Simple/Channel" 

321 
"Simple/Lift" 

322 
"Simple/Mutex" 

323 
"Simple/Reach" 

324 
"Simple/Reachability" 

325 

326 
(*Verifying security protocols using UNITY*) 

327 
"Simple/NSP_Bad" 

328 

329 
(*Example of composition*) 

330 
"Comp/Handshake" 

331 

332 
(*Universal properties examples*) 

333 
"Comp/Counter" 

334 
"Comp/Counterc" 

335 
"Comp/Priority" 

336 

337 
"Comp/TimerArray" 

338 
"Comp/Progress" 

339 

340 
"Comp/Alloc" 

341 
"Comp/AllocImpl" 

342 
"Comp/Client" 

343 

344 
(*obsolete*) 

345 
"ELT" 

346 
files "document/root.tex" 

347 

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

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

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 "HOLZF" in ZF = HOL + 
48481  354 
theories MainZF Games 
355 
files "document/root.tex" 

356 

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

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

360 
"~~/src/HOL/Library/Countable" 

361 
"~~/src/HOL/Library/Monad_Syntax" 

362 
"~~/src/HOL/Library/LaTeXsugar" 

363 
theories Imperative_HOL_ex 

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

365 

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

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

369 
*} 

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

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

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

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

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

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

377 
XML_Data 
48481  378 

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

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

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

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

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

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

388 
"~~/src/HOL/Number_Theory/UniqueFactorization" 

389 
"~~/src/HOL/Library/State_Monad" 

390 
theories 

391 
Greatest_Common_Divisor 

392 
Warshall 

393 
Higman_Extraction 

394 
Pigeonhole 

395 
Euclid 

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

397 

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

398 
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

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

400 
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

401 

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

402 
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

403 
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

404 

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

405 
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

406 
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

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

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

413 
StrongNorm 

414 
Standardization 

415 
WeakNorm 

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

417 

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

418 
session "HOLProlog" in Prolog = HOL + 
48481  419 
description {* 
420 
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

421 

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

422 
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

423 

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

424 
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

425 
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

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

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

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

431 
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

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

433 
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

434 
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

435 
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

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

439 
theories MicroJava 

440 
files 

441 
"document/introduction.tex" 

442 
"document/root.bib" 

443 
"document/root.tex" 

444 

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

445 
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

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

447 
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

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

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

452 

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

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

456 
AxExample 

457 
AxSound 

458 
AxCompl 

459 
Trans 

460 
files "document/root.tex" 

461 

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

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

464 
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

465 
Copyright 19941996 TU Muenchen 
48481  466 

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

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

468 
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

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

471 
@inproceedings{NipkowSlindIOA, 

472 
author={Tobias Nipkow and Konrad Slind}, 

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

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

475 
publisher=Springer, 

476 
series=LNCS, 

477 
note={To appear}} 

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

479 

480 
and 

481 

482 
@inproceedings{MuellerNipkow, 

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

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

485 
booktitle={Proc.\ TACAS Workshop}, 

486 
organization={Aarhus University, BRICS report}, 

487 
year=1995} 

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

489 
*} 

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

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

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

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

496 

497 
Basic theory of lattices and orders. 

498 
*} 

499 
theories CompleteLattice 

500 
files "document/root.tex" 

501 

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

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

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

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

505 
*} 
48679  506 
options [timeout = 3600, condition = ISABELLE_POLYML] 
48481  507 
theories [document = false] 
508 
"~~/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

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

512 
Normalization_by_Evaluation 

513 
Hebrew 

514 
Chinese 

515 
Serbian 

516 
"~~/src/HOL/Library/FinFun_Syntax" 

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

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

518 
Cartouche_Examples 
48481  519 
theories 
520 
Iff_Oracle 

521 
Coercion_Examples 

522 
Higher_Order_Logic 

523 
Abstract_NAT 

524 
Guess 

525 
Fundefs 

526 
Induction_Schema 

527 
LocaleTest2 

528 
Records 

529 
While_Combinator_Example 

530 
MonoidGroup 

531 
BinEx 

532 
Hex_Bin_Examples 

533 
Antiquote 

534 
Multiquote 

535 
PER 

536 
NatSum 

537 
ThreeDivides 

538 
Intuitionistic 

539 
CTL 

540 
Arith_Examples 

541 
BT 

542 
Tree23 

543 
MergeSort 

544 
Lagrange 

545 
Groebner_Examples 

546 
MT 

547 
Unification 

548 
Primrec 

549 
Tarski 

550 
Classical 

551 
Set_Theory 

552 
Termination 

553 
Coherent 

554 
PresburgerEx 

51093  555 
Reflection_Examples 
48481  556 
Sqrt 
557 
Sqrt_Script 

558 
Transfer_Ex 

559 
Transfer_Int_Nat 

560 
HarmonicSeries 

561 
Refute_Examples 

562 
Execute_Choice 

563 
Summation 

564 
Gauge_Integration 

565 
Dedekind_Real 

566 
Quicksort 

567 
Birthday_Paradox 

568 
List_to_Set_Comprehension_Examples 

569 
Seq 

570 
Simproc_Tests 

571 
Executable_Relation 

572 
FinFunPred 

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

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

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

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

585 
Sudoku 

586 
(* FIXME 

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

55240  588 
SAT_Examples 
48481  589 
*) 
590 
files "document/root.bib" "document/root.tex" 

591 

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

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

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

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

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

598 
"../Number_Theory/Primes" 

599 
theories 

600 
Basic_Logic 

601 
Cantor 

602 
Drinker 

603 
Expr_Compiler 

604 
Fibonacci 

605 
Group 

606 
Group_Context 

607 
Group_Notepad 

608 
Hoare_Ex 

609 
Knaster_Tarski 

610 
Mutilated_Checkerboard 

611 
Nested_Datatype 

612 
Peirce 

613 
Puzzle 

614 
Summation 

615 
files 

616 
"document/root.bib" 

617 
"document/root.tex" 

618 
"document/style.tex" 

619 

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

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

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

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

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

626 
theories SET_Protocol 

627 
files "document/root.tex" 

628 

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

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

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

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

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

635 
files "document/root.tex" 

636 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

659 
Author: Nik Sultana, University of Cambridge 

660 
Copyright 2011 

661 

662 
TPTPrelated extensions. 

663 
*} 

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

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

667 
MaSh_Eval 

668 
MaSh_Export 

669 
TPTP_Interpret 

670 
THF_Arith 

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

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

672 
theories 
48481  673 
ATP_Problem_Import 
674 

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

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

678 
Multivariate_Analysis 

679 
Determinants 

56215  680 
PolyRoots 
681 
Complex_Analysis_Basics 

48481  682 
files 
683 
"document/root.tex" 

684 

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

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

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

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

691 
theories 

692 
Probability 

693 
"ex/Dining_Cryptographers" 

694 
"ex/Koepf_Duermuth_Countermeasure" 

695 
files "document/root.tex" 

696 

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

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

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

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

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

705 

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

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

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

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

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

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

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

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

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

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

716 

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

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

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

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

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

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

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

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

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

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

731 
theories [condition = ISABELLE_FULL_TEST] 
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset

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

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

736 

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

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

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

741 

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

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

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

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

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

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

748 
StateSpaceEx 
48481  749 
files "document/root.tex" 
750 

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

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

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

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

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

757 
files "document/root.tex" 

758 

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

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

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

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

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

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

766 

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

767 
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

768 
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

769 
theories Ex 
48481  770 

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

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

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

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

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

778 
SMT_Tests 
48481  779 
files 
780 
"Boogie_Dijkstra.certs" 

781 
"Boogie_Max.certs" 

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

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

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

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

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

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

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

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

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

795 

796 
"Liseq/Longest_Increasing_Subsequence" 

797 

798 
"RIPEMD160/F" 

799 
"RIPEMD160/Hash" 

800 
"RIPEMD160/K_L" 

801 
"RIPEMD160/K_R" 

802 
"RIPEMD160/R_L" 

803 
"RIPEMD160/Round" 

804 
"RIPEMD160/R_R" 

805 
"RIPEMD160/S_L" 

806 
"RIPEMD160/S_R" 

807 

808 
"Sqrt/Sqrt" 

809 
files 

810 
"Gcd/greatest_common_divisor/g_c_d.fdl" 

811 
"Gcd/greatest_common_divisor/g_c_d.rls" 

812 
"Gcd/greatest_common_divisor/g_c_d.siv" 

813 
"Liseq/liseq/liseq_length.fdl" 

814 
"Liseq/liseq/liseq_length.rls" 

815 
"Liseq/liseq/liseq_length.siv" 

816 
"RIPEMD160/rmd/f.fdl" 

817 
"RIPEMD160/rmd/f.rls" 

818 
"RIPEMD160/rmd/f.siv" 

819 
"RIPEMD160/rmd/hash.fdl" 

820 
"RIPEMD160/rmd/hash.rls" 

821 
"RIPEMD160/rmd/hash.siv" 

822 
"RIPEMD160/rmd/k_l.fdl" 

823 
"RIPEMD160/rmd/k_l.rls" 

824 
"RIPEMD160/rmd/k_l.siv" 

825 
"RIPEMD160/rmd/k_r.fdl" 

826 
"RIPEMD160/rmd/k_r.rls" 

827 
"RIPEMD160/rmd/k_r.siv" 

828 
"RIPEMD160/rmd/r_l.fdl" 

829 
"RIPEMD160/rmd/r_l.rls" 

830 
"RIPEMD160/rmd/r_l.siv" 

831 
"RIPEMD160/rmd/round.fdl" 

832 
"RIPEMD160/rmd/round.rls" 

833 
"RIPEMD160/rmd/round.siv" 

834 
"RIPEMD160/rmd/r_r.fdl" 

835 
"RIPEMD160/rmd/r_r.rls" 

836 
"RIPEMD160/rmd/r_r.siv" 

837 
"RIPEMD160/rmd/s_l.fdl" 

838 
"RIPEMD160/rmd/s_l.rls" 

839 
"RIPEMD160/rmd/s_l.siv" 

840 
"RIPEMD160/rmd/s_r.fdl" 

841 
"RIPEMD160/rmd/s_r.rls" 

842 
"RIPEMD160/rmd/s_r.siv" 

843 

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

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

848 
VC_Principles 

849 
Reference 

850 
Complex_Types 

851 
files 

852 
"complex_types_app/initialize.fdl" 

853 
"complex_types_app/initialize.rls" 

854 
"complex_types_app/initialize.siv" 

855 
"document/complex_types.ads" 

856 
"document/complex_types_app.adb" 

857 
"document/complex_types_app.ads" 

858 
"document/Gcd.adb" 

859 
"document/Gcd.ads" 

860 
"document/intro.tex" 

861 
"document/loop_invariant.adb" 

862 
"document/loop_invariant.ads" 

863 
"document/root.bib" 

864 
"document/root.tex" 

865 
"document/Simple_Gcd.adb" 

866 
"document/Simple_Gcd.ads" 

867 
"loop_invariant/proc1.fdl" 

868 
"loop_invariant/proc1.rls" 

869 
"loop_invariant/proc1.siv" 

870 
"loop_invariant/proc2.fdl" 

871 
"loop_invariant/proc2.rls" 

872 
"loop_invariant/proc2.siv" 

873 
"simple_greatest_common_divisor/g_c_d.fdl" 

874 
"simple_greatest_common_divisor/g_c_d.rls" 

875 
"simple_greatest_common_divisor/g_c_d.siv" 

876 

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

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

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

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

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

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

886 
Quickcheck_Lattice_Examples 

887 
Completeness 

888 
Quickcheck_Interfaces 

889 
Hotel_Example *) 

48598  890 
theories [condition = ISABELLE_GHC] 
891 
Quickcheck_Narrowing_Examples 

48588  892 

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

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

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

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

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

897 
Needham_Schroeder_Guided_Attacker_Example 
48690  898 
Needham_Schroeder_Unguided_Attacker_Example 
48481  899 

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

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

903 
*} 

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

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

907 
FSet 

908 
Quotient_Int 

909 
Quotient_Message 

910 
Lift_FSet 

911 
Lift_Set 

912 
Lift_Fun 

913 
Quotient_Rat 

914 
Lift_DList 

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

915 
Int_Pow 
48481  916 

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

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

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

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

48481  924 
Specialisation_Examples 
48690  925 
IMP_1 
926 
IMP_2 

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

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

928 
Hotel_Example_Small_Generator 
48690  929 
IMP_3 
930 
IMP_4 *) 

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

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

934 
Hotel_Example_Prolog 

935 
Lambda_Example 

936 
List_Examples 

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

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

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

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

943 
Author: Brian Huffman 

944 

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

946 
*} 

947 
options [document_graph] 

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

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

48481  951 
theories 
952 
Plain_HOLCF 

953 
Fixrec 

954 
HOLCF 

955 
files "document/root.tex" 

956 

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

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

960 
Fixrec_ex 

961 
New_Domain 

962 
files "document/root.tex" 

963 

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

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

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

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

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

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

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

971 

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

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

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

974 
options [document = false] 
48481  975 
theories HoareEx 
48338  976 
files "document/root.tex" 
977 

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

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

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

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

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

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

985 
Dagstuhl 

986 
Focus_ex 

987 
Fix2 

988 
Hoare 

989 
Concurrency_Monad 

990 
Loop 

991 
Powerdomain_ex 

992 
Domain_Proofs 

993 
Letrec 

994 
Pattern_Match 

995 

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

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

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

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

999 

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

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

1001 

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

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

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

1004 

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

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

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

1007 

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

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

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

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

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

1014 
FOCUS 

1015 
Buffer_adm 

1016 

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

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

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

1020 
Copyright 1997 TU München 
48481  1021 

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

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

1023 

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

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

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

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

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

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

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

1034 

1035 
The Alternating Bit Protocol performed in I/OAutomata. 

1036 
*} 

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

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

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

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

1043 

1044 
A network transmission protocol, performed in the 

1045 
I/O automata formalization by Olaf Mueller. 

1046 
*} 

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

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

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

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

1053 

1054 
Memory storage case study. 

1055 
*} 

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

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

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

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

1062 
*} 

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

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

1066 
TrivEx2 

1067 

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

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

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

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

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

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

1076 
SML 

1077 
Verilog 

1078 

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

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

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

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

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

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