author  haftmann 
Mon, 10 Jun 2013 20:30:23 +0200  
changeset 52363  41d7946e2595 
parent 52282  c79a3e15779e 
child 52394  fe33d456b36c 
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 
*} 
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

19 
options [document = false, proofs = 2, skip_proofs = false] 
48338  20 
theories Main 
48901
5e0455e29339
more basic file dependencies  no load command here;
wenzelm
parents:
48765
diff
changeset

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

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

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

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

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

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

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

28 
*} 
48481  29 
theories 
30 
Library 

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

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

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

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

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

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

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

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

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

40 
Code_Char 
48721  41 
(* Code_Prolog FIXME cf. 76965c356d2a *) 
48481  42 
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

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

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

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

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

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

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

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

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

51 
Sum_of_Squares_Remote 
48481  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 "HOLHahn_Banach" in Hahn_Banach = HOL + 
48481  55 
description {* 
56 
Author: Gertrud Bauer, TU Munich 

57 

58 
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

59 

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

60 
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

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

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

63 
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

64 

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

65 
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

66 
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

67 

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

68 
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

69 
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

70 
continous linearform on the whole vectorspace. 
48481  71 
*} 
72 
options [document_graph] 

73 
theories Hahn_Banach 

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

75 

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

76 
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

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

78 
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

79 

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

80 
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

81 
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

82 

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

83 
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

84 
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

85 

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

86 
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

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

88 
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

89 

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

90 
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

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

92 
*} 
48481  93 
theories [quick_and_dirty] 
94 
Common_Patterns 

95 
theories 

96 
QuoDataType 

97 
QuoNestedDataType 

98 
Term 

99 
SList 

100 
ABexp 

101 
Tree 

102 
Ordinals 

103 
Sigma_Algebra 

104 
Comb 

105 
PropLog 

106 
Com 

107 
files "document/root.tex" 

108 

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

109 
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

110 
options [document_graph, document_variants=document] 
48481  111 
theories [document = false] 
112 
"~~/src/HOL/ex/Interpretation_with_Defs" 

113 
"~~/src/HOL/Library/While_Combinator" 

114 
"~~/src/HOL/Library/Char_ord" 

115 
"~~/src/HOL/Library/List_lexord" 

51625  116 
"~~/src/HOL/Library/Quotient_List" 
117 
"~~/src/HOL/Library/Extended" 

48481  118 
theories 
119 
BExp 

120 
ASM 

50050  121 
Finite_Reachable 
48481  122 
Denotation 
123 
Comp_Rev 

124 
Poly_Types 

125 
Sec_Typing 

126 
Sec_TypingT 

50161  127 
Def_Init_Sound_Big 
128 
Def_Init_Sound_Small 

48481  129 
Live 
130 
Live_True 

131 
Hoare_Examples 

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

135 
Collecting_Examples 
48481  136 
Abs_Int_Tests 
137 
Abs_Int1_parity 

138 
Abs_Int1_const 

139 
Abs_Int3 

140 
"Abs_Int_ITP/Abs_Int1_parity_ITP" 

141 
"Abs_Int_ITP/Abs_Int1_const_ITP" 

142 
"Abs_Int_ITP/Abs_Int3_ITP" 

143 
"Abs_Int_Den/Abs_Int_den2" 

144 
Procs_Dyn_Vars_Dyn 

145 
Procs_Stat_Vars_Dyn 

146 
Procs_Stat_Vars_Stat 

147 
C_like 

148 
OO 

149 
Fold 

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

151 

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

152 
session "HOLIMPP" in IMPP = HOL + 
48481  153 
description {* 
154 
Author: David von Oheimb 

155 
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

156 

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

157 
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

158 

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

159 
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

160 
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

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

163 
options [document = false] 
48481  164 
theories EvenOdd 
165 

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

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

169 
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 

170 

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

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

172 
options [document = false] 
48481  173 
theories Number_Theory 
174 

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

175 
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

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

177 
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

178 
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

179 
*} 
48481  180 
options [document_graph] 
181 
theories [document = false] 

182 
"~~/src/HOL/Library/Infinite_Set" 

183 
"~~/src/HOL/Library/Permutation" 

184 
theories 

185 
Fib 

186 
Factorization 

187 
Chinese 

188 
WilsonRuss 

189 
WilsonBij 

190 
Quadratic_Reciprocity 

191 
Primes 

192 
Pocklington 

193 
files "document/root.tex" 

194 

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

195 
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

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

197 
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

198 
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

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

200 

48481  201 
theories Hoare 
202 
files "document/root.bib" "document/root.tex" 

203 

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

204 
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

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

206 
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

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

208 
*} 
48481  209 
options [document_graph] 
210 
theories Hoare_Parallel 

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

212 

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

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

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

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

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

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

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

220 
Generate_Pretty_Char 
48481  221 

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

222 
session "HOLMetis_Examples" in Metis_Examples = HOL + 
48481  223 
description {* 
224 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

225 
Author: Jasmin Blanchette, TU Muenchen 

226 

227 
Testing Metis and Sledgehammer. 

228 
*} 

48679  229 
options [timeout = 3600, document = false] 
48481  230 
theories 
231 
Abstraction 

232 
Big_O 

233 
Binary_Tree 

234 
Clausification 

235 
Message 

236 
Proxies 

237 
Tarski 

238 
Trans_Closure 

239 
Sets 

240 

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

241 
session "HOLNitpick_Examples" in Nitpick_Examples = HOL + 
48481  242 
description {* 
243 
Author: Jasmin Blanchette, TU Muenchen 

244 
Copyright 2009 

245 
*} 

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

246 
options [document = false] 
48481  247 
theories [quick_and_dirty] Nitpick_Examples 
248 

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

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

252 

253 
The Isabelle Algebraic Library. 

254 
*} 

255 
options [document_graph] 

256 
theories [document = false] 

257 
(* Preliminaries from set and number theory *) 

258 
"~~/src/HOL/Library/FuncSet" 

259 
"~~/src/HOL/Old_Number_Theory/Primes" 

260 
"~~/src/HOL/Library/Binomial" 

261 
"~~/src/HOL/Library/Permutation" 

262 
theories 

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

264 
(* Groups *) 

265 
FiniteProduct (* Product operator for commutative groups *) 

266 
Sylow (* Sylow's theorem *) 

267 
Bij (* Automorphism Groups *) 

268 

269 
(* Rings *) 

270 
Divisibility (* Rings *) 

271 
IntRing (* Ideals and residue classes *) 

272 
UnivPoly (* Polynomials *) 

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

274 

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

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

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

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

278 
*} 
48481  279 
options [document_graph] 
280 
theories 

281 
Auth_Shared 

282 
Auth_Public 

283 
"Smartcard/Auth_Smartcard" 

284 
"Guard/Auth_Guard_Shared" 

285 
"Guard/Auth_Guard_Public" 

286 
files "document/root.tex" 

287 

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

288 
session "HOLUNITY" in UNITY = "HOLAuth" + 
48481  289 
description {* 
290 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

291 
Copyright 1998 University of Cambridge 

292 

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

293 
Verifying security protocols using Chandy and Misra's UNITY formalism. 
48481  294 
*} 
295 
options [document_graph] 

296 
theories 

297 
(*Basic metatheory*) 

298 
"UNITY_Main" 

299 

300 
(*Simple examples: no composition*) 

301 
"Simple/Deadlock" 

302 
"Simple/Common" 

303 
"Simple/Network" 

304 
"Simple/Token" 

305 
"Simple/Channel" 

306 
"Simple/Lift" 

307 
"Simple/Mutex" 

308 
"Simple/Reach" 

309 
"Simple/Reachability" 

310 

311 
(*Verifying security protocols using UNITY*) 

312 
"Simple/NSP_Bad" 

313 

314 
(*Example of composition*) 

315 
"Comp/Handshake" 

316 

317 
(*Universal properties examples*) 

318 
"Comp/Counter" 

319 
"Comp/Counterc" 

320 
"Comp/Priority" 

321 

322 
"Comp/TimerArray" 

323 
"Comp/Progress" 

324 

325 
"Comp/Alloc" 

326 
"Comp/AllocImpl" 

327 
"Comp/Client" 

328 

329 
(*obsolete*) 

330 
"ELT" 

331 
files "document/root.tex" 

332 

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

333 
session "HOLUnix" in Unix = HOL + 
48481  334 
options [print_mode = "no_brackets,no_type_brackets"] 
335 
theories Unix 

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

337 

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

338 
session "HOLZF" in ZF = HOL + 
48481  339 
theories MainZF Games 
340 
files "document/root.tex" 

341 

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

342 
session "HOLImperative_HOL" in Imperative_HOL = HOL + 
48481  343 
options [document_graph, print_mode = "iff,no_brackets"] 
344 
theories [document = false] 

345 
"~~/src/HOL/Library/Countable" 

346 
"~~/src/HOL/Library/Monad_Syntax" 

347 
"~~/src/HOL/Library/LaTeXsugar" 

348 
theories Imperative_HOL_ex 

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

350 

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

351 
session "HOLDecision_Procs" in Decision_Procs = HOL + 
51544  352 
description {* 
353 
Various decision procedures, typically involving reflection. 

354 
*} 

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

355 
options [condition = ISABELLE_POLYML, document = false] 
48481  356 
theories Decision_Procs 
357 

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

358 
session "HOLProofsex" in "Proofs/ex" = "HOLProofs" + 
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

359 
options [document = false, proofs = 2, skip_proofs = false, parallel_proofs = 0] 
48481  360 
theories Hilbert_Classical 
361 

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

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

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

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

365 
*} 
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

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

368 
"~~/src/HOL/Library/Code_Target_Numeral" 
48481  369 
"~~/src/HOL/Library/Monad_Syntax" 
370 
"~~/src/HOL/Number_Theory/Primes" 

371 
"~~/src/HOL/Number_Theory/UniqueFactorization" 

372 
"~~/src/HOL/Library/State_Monad" 

373 
theories 

374 
Greatest_Common_Divisor 

375 
Warshall 

376 
Higman_Extraction 

377 
Pigeonhole 

378 
Euclid 

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

380 

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

381 
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

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

383 
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

384 

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

385 
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

386 
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

387 

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

388 
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

389 
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

390 
*} 
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

391 
options [document_graph, print_mode = "no_brackets", proofs = 2, 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

392 
parallel_proofs = 0] 
48481  393 
theories [document = false] 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51115
diff
changeset

394 
"~~/src/HOL/Library/Code_Target_Int" 
48481  395 
theories 
396 
Eta 

397 
StrongNorm 

398 
Standardization 

399 
WeakNorm 

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

401 

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

402 
session "HOLProlog" in Prolog = HOL + 
48481  403 
description {* 
404 
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

405 

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

406 
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

407 

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

408 
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

409 
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

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

412 
options [document = false] 
48481  413 
theories Test Type 
414 

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

415 
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

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

417 
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

418 
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

419 
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

420 
*} 
48481  421 
options [document_graph] 
422 
theories [document = false] "~~/src/HOL/Library/While_Combinator" 

423 
theories MicroJava 

424 
files 

425 
"document/introduction.tex" 

426 
"document/root.bib" 

427 
"document/root.tex" 

428 

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

429 
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

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

431 
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

432 
*} 
48481  433 
options [document_graph] 
434 
theories Example 

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

436 

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

437 
session "HOLBali" in Bali = HOL + 
48481  438 
options [document_graph] 
439 
theories 

440 
AxExample 

441 
AxSound 

442 
AxCompl 

443 
Trans 

444 
files "document/root.tex" 

445 

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

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

448 
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

449 
Copyright 19941996 TU Muenchen 
48481  450 

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

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

452 
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

453 
proofs of two communication protocols which formerly have been here. 
48481  454 

455 
@inproceedings{NipkowSlindIOA, 

456 
author={Tobias Nipkow and Konrad Slind}, 

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

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

459 
publisher=Springer, 

460 
series=LNCS, 

461 
note={To appear}} 

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

463 

464 
and 

465 

466 
@inproceedings{MuellerNipkow, 

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

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

469 
booktitle={Proc.\ TACAS Workshop}, 

470 
organization={Aarhus University, BRICS report}, 

471 
year=1995} 

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

473 
*} 

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

474 
options [document = false] 
48481  475 
theories Solve 
476 

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

477 
session "HOLLattice" in Lattice = HOL + 
48481  478 
description {* 
479 
Author: Markus Wenzel, TU Muenchen 

480 

481 
Basic theory of lattices and orders. 

482 
*} 

483 
theories CompleteLattice 

484 
files "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 "HOLex" in ex = HOL + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

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

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

489 
*} 
48679  490 
options [timeout = 3600, condition = ISABELLE_POLYML] 
48481  491 
theories [document = false] 
492 
"~~/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

493 
Code_Binary_Nat_examples 
48481  494 
"~~/src/HOL/Library/FuncSet" 
495 
Eval_Examples 

496 
Normalization_by_Evaluation 

497 
Hebrew 

498 
Chinese 

499 
Serbian 

500 
"~~/src/HOL/Library/FinFun_Syntax" 

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

501 
"~~/src/HOL/Library/Refute" 
48481  502 
theories 
503 
Iff_Oracle 

504 
Coercion_Examples 

505 
Higher_Order_Logic 

506 
Abstract_NAT 

507 
Guess 

508 
Fundefs 

509 
Induction_Schema 

510 
LocaleTest2 

511 
Records 

512 
While_Combinator_Example 

513 
MonoidGroup 

514 
BinEx 

515 
Hex_Bin_Examples 

516 
Antiquote 

517 
Multiquote 

518 
PER 

519 
NatSum 

520 
ThreeDivides 

521 
Intuitionistic 

522 
CTL 

523 
Arith_Examples 

524 
BT 

525 
Tree23 

526 
MergeSort 

527 
Lagrange 

528 
Groebner_Examples 

529 
MT 

530 
Unification 

531 
Primrec 

532 
Tarski 

533 
Classical 

534 
Set_Theory 

535 
Termination 

536 
Coherent 

537 
PresburgerEx 

51093  538 
Reflection_Examples 
48481  539 
Sqrt 
540 
Sqrt_Script 

541 
Transfer_Ex 

542 
Transfer_Int_Nat 

543 
HarmonicSeries 

544 
Refute_Examples 

545 
Execute_Choice 

546 
Summation 

547 
Gauge_Integration 

548 
Dedekind_Real 

549 
Quicksort 

550 
Birthday_Paradox 

551 
List_to_Set_Comprehension_Examples 

552 
Seq 

553 
Simproc_Tests 

554 
Executable_Relation 

555 
FinFunPred 

556 
Set_Comprehension_Pointfree_Tests 

557 
Parallel_Example 

50138  558 
IArray_Examples 
51559  559 
SVC_Oracle 
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

560 
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

561 
Meson_Test 
48690  562 
theories [condition = SVC_HOME] 
563 
svc_test 

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

566 
Sudoku 

567 
(* FIXME 

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

569 
(*global sideeffects ahead!*) 

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

571 
*) 

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

573 

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

574 
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

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

576 
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

577 
*} 
48481  578 
theories [document = false] 
579 
"~~/src/HOL/Library/Lattice_Syntax" 

580 
"../Number_Theory/Primes" 

581 
theories 

582 
Basic_Logic 

583 
Cantor 

584 
Drinker 

585 
Expr_Compiler 

586 
Fibonacci 

587 
Group 

588 
Group_Context 

589 
Group_Notepad 

590 
Hoare_Ex 

591 
Knaster_Tarski 

592 
Mutilated_Checkerboard 

593 
Nested_Datatype 

594 
Peirce 

595 
Puzzle 

596 
Summation 

597 
files 

598 
"document/root.bib" 

599 
"document/root.tex" 

600 
"document/style.tex" 

601 

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

602 
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

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

604 
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

605 
*} 
48481  606 
options [document_graph] 
607 
theories [document = false] "~~/src/HOL/Library/Nat_Bijection" 

608 
theories SET_Protocol 

609 
files "document/root.tex" 

610 

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

611 
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

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

613 
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

614 
*} 
48481  615 
options [document_graph] 
616 
theories Cplex 

617 
files "document/root.tex" 

618 

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

619 
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

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

621 
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

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

623 
options [document = false] 
48481  624 
theories TLA 
625 

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

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

627 
options [document = false] 
48481  628 
theories Inc 
629 

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

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

631 
options [document = false] 
48481  632 
theories DBuffer 
633 

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

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

635 
options [document = false] 
48481  636 
theories MemoryImplementation 
637 

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

638 
session "HOLTPTP" in TPTP = HOL + 
48481  639 
description {* 
640 
Author: Jasmin Blanchette, TU Muenchen 

641 
Author: Nik Sultana, University of Cambridge 

642 
Copyright 2011 

643 

644 
TPTPrelated extensions. 

645 
*} 

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

646 
options [document = false] 
48481  647 
theories 
648 
ATP_Theory_Export 

649 
MaSh_Eval 

650 
MaSh_Export 

651 
TPTP_Interpret 

652 
THF_Arith 

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

654 
ATP_Problem_Import 

655 

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

656 
session "HOLMultivariate_Analysis" (main) in Multivariate_Analysis = HOL + 
48481  657 
options [document_graph] 
658 
theories 

659 
Multivariate_Analysis 

660 
Determinants 

661 
files 

662 
"document/root.tex" 

663 

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

664 
session "HOLProbability" in "Probability" = "HOLMultivariate_Analysis" + 
48617  665 
options [document_graph] 
48481  666 
theories [document = false] 
667 
"~~/src/HOL/Library/Countable" 

668 
"~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits" 

669 
"~~/src/HOL/Library/Permutation" 

670 
theories 

671 
Probability 

672 
"ex/Dining_Cryptographers" 

673 
"ex/Koepf_Duermuth_Countermeasure" 

674 
files "document/root.tex" 

675 

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

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

677 
options [document = false] 
48481  678 
theories Nominal 
679 

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

680 
session "HOLNominalExamples" in "Nominal/Examples" = "HOLNominal" + 
48679  681 
options [timeout = 3600, condition = ISABELLE_POLYML, document = false] 
48481  682 
theories Nominal_Examples 
683 
theories [quick_and_dirty] VC_Condition 

684 

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

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

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

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

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

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

691 

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

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

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

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

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

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

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

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

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

702 

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

703 
session "HOLBNFLFP" in BNF = "HOLCardinalsBase" + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

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

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

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

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

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

709 

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

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

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

712 
Bounded Natural Functors for (Co)datatypes. 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

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

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

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

716 

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

717 
session "HOLBNFExamples" in "BNF/Examples" = "HOLBNF" + 
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 
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset

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

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

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

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

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

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

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

732 

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

733 
session "HOLWord" (main) in Word = HOL + 
48481  734 
options [document_graph] 
735 
theories Word 

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

737 

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

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

739 
options [document = false] 
48481  740 
theories WordExamples 
741 

52248
2c893e0c1def
added Spec_Check  a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
52226
diff
changeset

742 
session "HOLSpec_Check" in Spec_Check = HOL + 
2c893e0c1def
added Spec_Check  a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
52226
diff
changeset

743 
theories 
52277  744 
Spec_Check 
745 
theories [condition = ISABELLE_POLYML] 

52248
2c893e0c1def
added Spec_Check  a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
52226
diff
changeset

746 
Examples 
2c893e0c1def
added Spec_Check  a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
52226
diff
changeset

747 

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

748 
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

749 
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

750 
StateSpaceEx 
48481  751 
files "document/root.tex" 
752 

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

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

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

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

756 
*} 
48481  757 
options [document_graph] 
758 
theories Hypercomplex 

759 
files "document/root.tex" 

760 

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

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

762 
options [document = false] 
48481  763 
theories NSPrimes 
764 

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

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

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

768 

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

769 
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

770 
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

771 
theories Ex 
48481  772 

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

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

774 
options [document = false, quick_and_dirty] 
48481  775 
theories 
776 
SMT_Examples 

777 
SMT_Word_Examples 

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

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

779 
SMT_Tests 
48481  780 
files 
781 
"SMT_Examples.certs" 

50665  782 
"SMT_Word_Examples.certs" 
48481  783 

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

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

785 
options [document = false] 
48481  786 
theories Boogie 
787 

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

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

789 
options [document = false] 
48481  790 
theories 
791 
Boogie_Max_Stepwise 

792 
Boogie_Max 

793 
Boogie_Dijkstra 

794 
VCC_Max 

795 
files 

48493  796 
"Boogie_Dijkstra.b2i" 
48481  797 
"Boogie_Dijkstra.certs" 
48493  798 
"Boogie_Max.b2i" 
48481  799 
"Boogie_Max.certs" 
48493  800 
"VCC_Max.b2i" 
48481  801 
"VCC_Max.certs" 
802 

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

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

804 
options [document = false] 
48481  805 
theories SPARK 
806 

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

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

808 
options [document = false] 
48481  809 
theories 
810 
"Gcd/Greatest_Common_Divisor" 

811 

812 
"Liseq/Longest_Increasing_Subsequence" 

813 

814 
"RIPEMD160/F" 

815 
"RIPEMD160/Hash" 

816 
"RIPEMD160/K_L" 

817 
"RIPEMD160/K_R" 

818 
"RIPEMD160/R_L" 

819 
"RIPEMD160/Round" 

820 
"RIPEMD160/R_R" 

821 
"RIPEMD160/S_L" 

822 
"RIPEMD160/S_R" 

823 

824 
"Sqrt/Sqrt" 

825 
files 

826 
"Gcd/greatest_common_divisor/g_c_d.fdl" 

827 
"Gcd/greatest_common_divisor/g_c_d.rls" 

828 
"Gcd/greatest_common_divisor/g_c_d.siv" 

829 
"Liseq/liseq/liseq_length.fdl" 

830 
"Liseq/liseq/liseq_length.rls" 

831 
"Liseq/liseq/liseq_length.siv" 

832 
"RIPEMD160/rmd/f.fdl" 

833 
"RIPEMD160/rmd/f.rls" 

834 
"RIPEMD160/rmd/f.siv" 

835 
"RIPEMD160/rmd/hash.fdl" 

836 
"RIPEMD160/rmd/hash.rls" 

837 
"RIPEMD160/rmd/hash.siv" 

838 
"RIPEMD160/rmd/k_l.fdl" 

839 
"RIPEMD160/rmd/k_l.rls" 

840 
"RIPEMD160/rmd/k_l.siv" 

841 
"RIPEMD160/rmd/k_r.fdl" 

842 
"RIPEMD160/rmd/k_r.rls" 

843 
"RIPEMD160/rmd/k_r.siv" 

844 
"RIPEMD160/rmd/r_l.fdl" 

845 
"RIPEMD160/rmd/r_l.rls" 

846 
"RIPEMD160/rmd/r_l.siv" 

847 
"RIPEMD160/rmd/round.fdl" 

848 
"RIPEMD160/rmd/round.rls" 

849 
"RIPEMD160/rmd/round.siv" 

850 
"RIPEMD160/rmd/r_r.fdl" 

851 
"RIPEMD160/rmd/r_r.rls" 

852 
"RIPEMD160/rmd/r_r.siv" 

853 
"RIPEMD160/rmd/s_l.fdl" 

854 
"RIPEMD160/rmd/s_l.rls" 

855 
"RIPEMD160/rmd/s_l.siv" 

856 
"RIPEMD160/rmd/s_r.fdl" 

857 
"RIPEMD160/rmd/s_r.rls" 

858 
"RIPEMD160/rmd/s_r.siv" 

859 

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

860 
session "HOLSPARKManual" in "SPARK/Manual" = "HOLSPARK" + 
48486  861 
options [show_question_marks = false] 
48481  862 
theories 
863 
Example_Verification 

864 
VC_Principles 

865 
Reference 

866 
Complex_Types 

867 
files 

868 
"complex_types_app/initialize.fdl" 

869 
"complex_types_app/initialize.rls" 

870 
"complex_types_app/initialize.siv" 

871 
"document/complex_types.ads" 

872 
"document/complex_types_app.adb" 

873 
"document/complex_types_app.ads" 

874 
"document/Gcd.adb" 

875 
"document/Gcd.ads" 

876 
"document/intro.tex" 

877 
"document/loop_invariant.adb" 

878 
"document/loop_invariant.ads" 

879 
"document/root.bib" 

880 
"document/root.tex" 

881 
"document/Simple_Gcd.adb" 

882 
"document/Simple_Gcd.ads" 

883 
"loop_invariant/proc1.fdl" 

884 
"loop_invariant/proc1.rls" 

885 
"loop_invariant/proc1.siv" 

886 
"loop_invariant/proc2.fdl" 

887 
"loop_invariant/proc2.rls" 

888 
"loop_invariant/proc2.siv" 

889 
"simple_greatest_common_divisor/g_c_d.fdl" 

890 
"simple_greatest_common_divisor/g_c_d.rls" 

891 
"simple_greatest_common_divisor/g_c_d.siv" 

892 

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

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

894 
options [document = false] 
48481  895 
theories MutabelleExtra 
896 

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

897 
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

898 
options [document = false] 
48588  899 
theories 
48690  900 
Quickcheck_Examples 
901 
(* FIXME 

902 
Quickcheck_Lattice_Examples 

903 
Completeness 

904 
Quickcheck_Interfaces 

905 
Hotel_Example *) 

48598  906 
theories [condition = ISABELLE_GHC] 
907 
Quickcheck_Narrowing_Examples 

48588  908 

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

909 
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

910 
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

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

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

913 
Needham_Schroeder_Guided_Attacker_Example 
48690  914 
Needham_Schroeder_Unguided_Attacker_Example 
48481  915 

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

916 
session "HOLQuotient_Examples" in Quotient_Examples = HOL + 
48481  917 
description {* 
918 
Author: Cezary Kaliszyk and Christian Urban 

919 
*} 

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

920 
options [document = false] 
48481  921 
theories 
922 
DList 

923 
FSet 

924 
Quotient_Int 

925 
Quotient_Message 

926 
Lift_FSet 

927 
Lift_Set 

928 
Lift_Fun 

929 
Quotient_Rat 

930 
Lift_DList 

931 

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

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

933 
options [document = false] 
48690  934 
theories 
48481  935 
Examples 
936 
Predicate_Compile_Tests 

48690  937 
(* FIXME 
938 
Predicate_Compile_Quickcheck_Examples  should be added again soon (since 21Oct2010) *) 

48481  939 
Specialisation_Examples 
48690  940 
(* FIXME since 21Jul2011 
941 
Hotel_Example_Small_Generator 

942 
IMP_1 

943 
IMP_2 

944 
IMP_3 

945 
IMP_4 *) 

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

947 
Code_Prolog_Examples 

948 
Context_Free_Grammar_Example 

949 
Hotel_Example_Prolog 

950 
Lambda_Example 

951 
List_Examples 

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

953 
Reg_Exp_Example 

48481  954 

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

955 
session HOLCF (main) in HOLCF = HOL + 
48338  956 
description {* 
957 
Author: Franz Regensburger 

958 
Author: Brian Huffman 

959 

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

961 
*} 

962 
options [document_graph] 

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

963 
theories [document = false] 
48338  964 
"~~/src/HOL/Library/Nat_Bijection" 
965 
"~~/src/HOL/Library/Countable" 

48481  966 
theories 
967 
Plain_HOLCF 

968 
Fixrec 

969 
HOLCF 

970 
files "document/root.tex" 

971 

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

972 
session "HOLCFTutorial" in "HOLCF/Tutorial" = HOLCF + 
48481  973 
theories 
974 
Domain_ex 

975 
Fixrec_ex 

976 
New_Domain 

977 
files "document/root.tex" 

978 

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

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

980 
options [document = false] 
48481  981 
theories HOLCF_Library 
982 

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

983 
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

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

985 
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

986 

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

987 
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

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

989 
options [document = false] 
48481  990 
theories HoareEx 
48338  991 
files "document/root.tex" 
992 

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

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

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

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

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

997 
options [document = false] 
48481  998 
theories 
999 
Dnat 

1000 
Dagstuhl 

1001 
Focus_ex 

1002 
Fix2 

1003 
Hoare 

1004 
Concurrency_Monad 

1005 
Loop 

1006 
Powerdomain_ex 

1007 
Domain_Proofs 

1008 
Letrec 

1009 
Pattern_Match 

1010 

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

1011 
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

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

1013 
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

1014 

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

1015 
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

1016 

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

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

1018 
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

1019 

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

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

1021 
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

1022 

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

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

1024 
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

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

1026 
options [document = false] 
48481  1027 
theories 
1028 
Fstreams 

1029 
FOCUS 

1030 
Buffer_adm 

1031 

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

1032 
session IOA in "HOLCF/IOA" = HOLCF + 
48481  1033 
description {* 
1034 
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

1035 
Copyright 1997 TU München 
48481  1036 

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

1037 
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

1038 

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

1039 
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

1040 
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

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

1043 
options [document = false] 
48481  1044 
theories "meta_theory/Abstraction" 
1045 

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

1046 
session "IOAABP" in "HOLCF/IOA/ABP" = IOA + 
48481  1047 
description {* 
1048 
Author: Olaf Mueller 

1049 

1050 
The Alternating Bit Protocol performed in I/OAutomata. 

1051 
*} 

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

1052 
options [document = false] 
48481  1053 
theories Correctness 
1054 

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

1055 
session "IOANTP" in "HOLCF/IOA/NTP" = IOA + 
48481  1056 
description {* 
1057 
Author: Tobias Nipkow & Konrad Slind 

1058 

1059 
A network transmission protocol, performed in the 

1060 
I/O automata formalization by Olaf Mueller. 

1061 
*} 

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

1062 
options [document = false] 
48481  1063 
theories Correctness 
1064 

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

1065 
session "IOAStorage" in "HOLCF/IOA/Storage" = IOA + 
48481  1066 
description {* 
1067 
Author: Olaf Mueller 

1068 

1069 
Memory storage case study. 

1070 
*} 

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

1071 
options [document = false] 
48481  1072 
theories Correctness 
1073 

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

1074 
session "IOAex" in "HOLCF/IOA/ex" = IOA + 
48481  1075 
description {* 
1076 
Author: Olaf Mueller 

1077 
*} 

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

1078 
options [document = false] 
48481  1079 
theories 
1080 
TrivEx 

1081 
TrivEx2 

1082 

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

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

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

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

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

1087 
options [document = false] 
48635  1088 
theories [condition = ISABELLE_FULL_TEST, timing] 
48481  1089 
Brackin 
1090 
Instructions 

1091 
SML 

1092 
Verilog 

1093 

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

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

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

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

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

1098 
options [document = false] 
48635  1099 
theories [condition = ISABELLE_FULL_TEST, timing] 
48481  1100 
Record_Benchmark 
1101 