author  blanchet 
Mon, 20 Jan 2014 18:24:56 +0100  
changeset 55071  8ae6f86a3477 
parent 55064  8dd21c4b0501 
child 55072  8488fdc4ddc0 
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 
48721  42 
(* Code_Prolog FIXME cf. 76965c356d2a *) 
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] 
114 
"~~/src/HOL/ex/Interpretation_with_Defs" 

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 + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

174 
options [document = false] 
48481  175 
theories Number_Theory 
176 

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

177 
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

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

179 
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

180 
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

181 
*} 
48481  182 
options [document_graph] 
183 
theories [document = false] 

184 
"~~/src/HOL/Library/Infinite_Set" 

185 
"~~/src/HOL/Library/Permutation" 

186 
theories 

187 
Fib 

188 
Factorization 

189 
Chinese 

190 
WilsonRuss 

191 
WilsonBij 

192 
Quadratic_Reciprocity 

193 
Primes 

194 
Pocklington 

195 
files "document/root.tex" 

196 

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

197 
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

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

199 
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

200 
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

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

202 

48481  203 
theories Hoare 
204 
files "document/root.bib" "document/root.tex" 

205 

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

206 
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

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

208 
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

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

210 
*} 
48481  211 
options [document_graph] 
212 
theories Hoare_Parallel 

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

214 

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

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

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

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

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

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

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

222 
Generate_Pretty_Char 
48481  223 

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

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

227 
Author: Jasmin Blanchette, TU Muenchen 

228 

229 
Testing Metis and Sledgehammer. 

230 
*} 

48679  231 
options [timeout = 3600, document = false] 
48481  232 
theories 
233 
Abstraction 

234 
Big_O 

235 
Binary_Tree 

236 
Clausification 

237 
Message 

238 
Proxies 

239 
Tarski 

240 
Trans_Closure 

241 
Sets 

242 

53808  243 
session "HOLBNFNitpick_Examples" in Nitpick_Examples = "HOLBNF" + 
48481  244 
description {* 
245 
Author: Jasmin Blanchette, TU Muenchen 

246 
Copyright 2009 

247 
*} 

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

248 
options [document = false] 
48481  249 
theories [quick_and_dirty] Nitpick_Examples 
250 

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

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

254 

255 
The Isabelle Algebraic Library. 

256 
*} 

257 
options [document_graph] 

258 
theories [document = false] 

259 
(* Preliminaries from set and number theory *) 

260 
"~~/src/HOL/Library/FuncSet" 

261 
"~~/src/HOL/Old_Number_Theory/Primes" 

262 
"~~/src/HOL/Library/Binomial" 

263 
"~~/src/HOL/Library/Permutation" 

264 
theories 

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

266 
(* Groups *) 

267 
FiniteProduct (* Product operator for commutative groups *) 

268 
Sylow (* Sylow's theorem *) 

269 
Bij (* Automorphism Groups *) 

270 

271 
(* Rings *) 

272 
Divisibility (* Rings *) 

273 
IntRing (* Ideals and residue classes *) 

274 
UnivPoly (* Polynomials *) 

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

276 

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

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

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

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

280 
*} 
48481  281 
options [document_graph] 
282 
theories 

283 
Auth_Shared 

284 
Auth_Public 

285 
"Smartcard/Auth_Smartcard" 

286 
"Guard/Auth_Guard_Shared" 

287 
"Guard/Auth_Guard_Public" 

288 
files "document/root.tex" 

289 

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

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

293 
Copyright 1998 University of Cambridge 

294 

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

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

298 
theories 

299 
(*Basic metatheory*) 

300 
"UNITY_Main" 

301 

302 
(*Simple examples: no composition*) 

303 
"Simple/Deadlock" 

304 
"Simple/Common" 

305 
"Simple/Network" 

306 
"Simple/Token" 

307 
"Simple/Channel" 

308 
"Simple/Lift" 

309 
"Simple/Mutex" 

310 
"Simple/Reach" 

311 
"Simple/Reachability" 

312 

313 
(*Verifying security protocols using UNITY*) 

314 
"Simple/NSP_Bad" 

315 

316 
(*Example of composition*) 

317 
"Comp/Handshake" 

318 

319 
(*Universal properties examples*) 

320 
"Comp/Counter" 

321 
"Comp/Counterc" 

322 
"Comp/Priority" 

323 

324 
"Comp/TimerArray" 

325 
"Comp/Progress" 

326 

327 
"Comp/Alloc" 

328 
"Comp/AllocImpl" 

329 
"Comp/Client" 

330 

331 
(*obsolete*) 

332 
"ELT" 

333 
files "document/root.tex" 

334 

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

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

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

339 

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

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

343 

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

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

347 
"~~/src/HOL/Library/Countable" 

348 
"~~/src/HOL/Library/Monad_Syntax" 

349 
"~~/src/HOL/Library/LaTeXsugar" 

350 
theories Imperative_HOL_ex 

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 "HOLDecision_Procs" in Decision_Procs = HOL + 
51544  354 
description {* 
355 
Various decision procedures, typically involving reflection. 

356 
*} 

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

357 
options [condition = ISABELLE_POLYML, document = false] 
48481  358 
theories Decision_Procs 
359 

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

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

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

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

364 
XML_Data 
48481  365 

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

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

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

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

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

372 
"~~/src/HOL/Library/Code_Target_Numeral" 
48481  373 
"~~/src/HOL/Library/Monad_Syntax" 
374 
"~~/src/HOL/Number_Theory/Primes" 

375 
"~~/src/HOL/Number_Theory/UniqueFactorization" 

376 
"~~/src/HOL/Library/State_Monad" 

377 
theories 

378 
Greatest_Common_Divisor 

379 
Warshall 

380 
Higman_Extraction 

381 
Pigeonhole 

382 
Euclid 

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

384 

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

385 
session "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

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

387 
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

388 

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

389 
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

390 
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

391 

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

392 
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

393 
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

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

397 
"~~/src/HOL/Library/Code_Target_Int" 
48481  398 
theories 
399 
Eta 

400 
StrongNorm 

401 
Standardization 

402 
WeakNorm 

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

404 

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

405 
session "HOLProlog" in Prolog = HOL + 
48481  406 
description {* 
407 
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

408 

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

409 
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

410 

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

411 
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

412 
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

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

415 
options [document = false] 
48481  416 
theories Test Type 
417 

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

418 
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

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

420 
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

421 
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

422 
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

423 
*} 
48481  424 
options [document_graph] 
425 
theories [document = false] "~~/src/HOL/Library/While_Combinator" 

426 
theories MicroJava 

427 
files 

428 
"document/introduction.tex" 

429 
"document/root.bib" 

430 
"document/root.tex" 

431 

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

432 
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

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

434 
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

435 
*} 
48481  436 
options [document_graph] 
437 
theories Example 

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

439 

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

440 
session "HOLBali" in Bali = HOL + 
48481  441 
options [document_graph] 
442 
theories 

443 
AxExample 

444 
AxSound 

445 
AxCompl 

446 
Trans 

447 
files "document/root.tex" 

448 

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

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

451 
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

452 
Copyright 19941996 TU Muenchen 
48481  453 

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

454 
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

455 
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

456 
proofs of two communication protocols which formerly have been here. 
48481  457 

458 
@inproceedings{NipkowSlindIOA, 

459 
author={Tobias Nipkow and Konrad Slind}, 

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

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

462 
publisher=Springer, 

463 
series=LNCS, 

464 
note={To appear}} 

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

466 

467 
and 

468 

469 
@inproceedings{MuellerNipkow, 

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

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

472 
booktitle={Proc.\ TACAS Workshop}, 

473 
organization={Aarhus University, BRICS report}, 

474 
year=1995} 

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

476 
*} 

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

477 
options [document = false] 
48481  478 
theories Solve 
479 

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

480 
session "HOLLattice" in Lattice = HOL + 
48481  481 
description {* 
482 
Author: Markus Wenzel, TU Muenchen 

483 

484 
Basic theory of lattices and orders. 

485 
*} 

486 
theories CompleteLattice 

487 
files "document/root.tex" 

488 

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

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

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

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

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

496 
Code_Binary_Nat_examples 
48481  497 
"~~/src/HOL/Library/FuncSet" 
498 
Eval_Examples 

499 
Normalization_by_Evaluation 

500 
Hebrew 

501 
Chinese 

502 
Serbian 

503 
"~~/src/HOL/Library/FinFun_Syntax" 

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

504 
"~~/src/HOL/Library/Refute" 
48481  505 
theories 
506 
Iff_Oracle 

507 
Coercion_Examples 

508 
Higher_Order_Logic 

509 
Abstract_NAT 

510 
Guess 

511 
Fundefs 

512 
Induction_Schema 

513 
LocaleTest2 

514 
Records 

515 
While_Combinator_Example 

516 
MonoidGroup 

517 
BinEx 

518 
Hex_Bin_Examples 

519 
Antiquote 

520 
Multiquote 

521 
PER 

522 
NatSum 

523 
ThreeDivides 

524 
Intuitionistic 

525 
CTL 

526 
Arith_Examples 

527 
BT 

528 
Tree23 

529 
MergeSort 

530 
Lagrange 

531 
Groebner_Examples 

532 
MT 

533 
Unification 

534 
Primrec 

535 
Tarski 

536 
Classical 

537 
Set_Theory 

538 
Termination 

539 
Coherent 

540 
PresburgerEx 

51093  541 
Reflection_Examples 
48481  542 
Sqrt 
543 
Sqrt_Script 

544 
Transfer_Ex 

545 
Transfer_Int_Nat 

546 
HarmonicSeries 

547 
Refute_Examples 

548 
Execute_Choice 

549 
Summation 

550 
Gauge_Integration 

551 
Dedekind_Real 

552 
Quicksort 

553 
Birthday_Paradox 

554 
List_to_Set_Comprehension_Examples 

555 
Seq 

556 
Simproc_Tests 

557 
Executable_Relation 

558 
FinFunPred 

559 
Set_Comprehension_Pointfree_Tests 

560 
Parallel_Example 

50138  561 
IArray_Examples 
51559  562 
SVC_Oracle 
53430  563 
Simps_Case_Conv_Examples 
53935  564 
ML 
55033  565 
Cartouche_Examples 
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

566 
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

567 
Meson_Test 
48690  568 
theories [condition = SVC_HOME] 
569 
svc_test 

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

572 
Sudoku 

573 
(* FIXME 

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

575 
(*global sideeffects ahead!*) 

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

577 
*) 

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

579 

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

580 
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

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

582 
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

583 
*} 
48481  584 
theories [document = false] 
585 
"~~/src/HOL/Library/Lattice_Syntax" 

586 
"../Number_Theory/Primes" 

587 
theories 

588 
Basic_Logic 

589 
Cantor 

590 
Drinker 

591 
Expr_Compiler 

592 
Fibonacci 

593 
Group 

594 
Group_Context 

595 
Group_Notepad 

596 
Hoare_Ex 

597 
Knaster_Tarski 

598 
Mutilated_Checkerboard 

599 
Nested_Datatype 

600 
Peirce 

601 
Puzzle 

602 
Summation 

603 
files 

604 
"document/root.bib" 

605 
"document/root.tex" 

606 
"document/style.tex" 

607 

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

608 
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

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

610 
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

611 
*} 
48481  612 
options [document_graph] 
613 
theories [document = false] "~~/src/HOL/Library/Nat_Bijection" 

614 
theories SET_Protocol 

615 
files "document/root.tex" 

616 

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

617 
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

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

619 
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

620 
*} 
48481  621 
options [document_graph] 
622 
theories Cplex 

623 
files "document/root.tex" 

624 

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

625 
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

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

627 
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

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

629 
options [document = false] 
48481  630 
theories TLA 
631 

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

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

633 
options [document = false] 
48481  634 
theories Inc 
635 

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

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

637 
options [document = false] 
48481  638 
theories DBuffer 
639 

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

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

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

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

644 
session "HOLTPTP" in TPTP = HOL + 
48481  645 
description {* 
646 
Author: Jasmin Blanchette, TU Muenchen 

647 
Author: Nik Sultana, University of Cambridge 

648 
Copyright 2011 

649 

650 
TPTPrelated extensions. 

651 
*} 

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

652 
options [document = false] 
48481  653 
theories 
654 
ATP_Theory_Export 

655 
MaSh_Eval 

656 
MaSh_Export 

657 
TPTP_Interpret 

658 
THF_Arith 

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

659 
theories 
48481  660 
ATP_Problem_Import 
661 

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

662 
session "HOLMultivariate_Analysis" (main) in Multivariate_Analysis = HOL + 
48481  663 
options [document_graph] 
664 
theories 

665 
Multivariate_Analysis 

666 
Determinants 

667 
files 

668 
"document/root.tex" 

669 

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

670 
session "HOLProbability" in "Probability" = "HOLMultivariate_Analysis" + 
48617  671 
options [document_graph] 
48481  672 
theories [document = false] 
673 
"~~/src/HOL/Library/Countable" 

674 
"~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits" 

675 
"~~/src/HOL/Library/Permutation" 

676 
theories 

677 
Probability 

678 
"ex/Dining_Cryptographers" 

679 
"ex/Koepf_Duermuth_Countermeasure" 

680 
files "document/root.tex" 

681 

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

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

683 
options [document = false] 
48481  684 
theories Nominal 
685 

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

686 
session "HOLNominalExamples" in "Nominal/Examples" = "HOLNominal" + 
48679  687 
options [timeout = 3600, condition = ISABELLE_POLYML, document = false] 
48481  688 
theories Nominal_Examples 
689 
theories [quick_and_dirty] VC_Condition 

690 

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

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

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

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

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

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

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

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

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

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

701 

55064  702 
session "HOLBNF" in BNF = HOL + 
54474  703 
description {* 
54481  704 
Bounded Natural Functors for (Co)datatypes, Including More BNFs. 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

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

706 
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

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

708 

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

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

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

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

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

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

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

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

717 
TreeFsetI 
49872  718 
"Derivation_Trees/Gram_Lang" 
719 
"Derivation_Trees/Parallel" 

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

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

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

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

727 

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

728 
session "HOLWord" (main) in Word = HOL + 
48481  729 
options [document_graph] 
730 
theories Word 

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

732 

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

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

734 
options [document = false] 
48481  735 
theories WordExamples 
736 

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

737 
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

738 
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

739 
StateSpaceEx 
48481  740 
files "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 "HOLNSA" in NSA = HOL + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

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

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

745 
*} 
48481  746 
options [document_graph] 
747 
theories Hypercomplex 

748 
files "document/root.tex" 

749 

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

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

751 
options [document = false] 
48481  752 
theories NSPrimes 
753 

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

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

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

757 

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

758 
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

759 
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

760 
theories Ex 
48481  761 

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

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

763 
options [document = false, quick_and_dirty] 
48481  764 
theories 
52722  765 
Boogie 
48481  766 
SMT_Examples 
767 
SMT_Word_Examples 

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

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

769 
SMT_Tests 
48481  770 
files 
771 
"Boogie_Dijkstra.certs" 

772 
"Boogie_Max.certs" 

52722  773 
"SMT_Examples.certs" 
774 
"SMT_Word_Examples.certs" 

48481  775 
"VCC_Max.certs" 
776 

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

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

778 
options [document = false] 
48481  779 
theories SPARK 
780 

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

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

782 
options [document = false] 
48481  783 
theories 
784 
"Gcd/Greatest_Common_Divisor" 

785 

786 
"Liseq/Longest_Increasing_Subsequence" 

787 

788 
"RIPEMD160/F" 

789 
"RIPEMD160/Hash" 

790 
"RIPEMD160/K_L" 

791 
"RIPEMD160/K_R" 

792 
"RIPEMD160/R_L" 

793 
"RIPEMD160/Round" 

794 
"RIPEMD160/R_R" 

795 
"RIPEMD160/S_L" 

796 
"RIPEMD160/S_R" 

797 

798 
"Sqrt/Sqrt" 

799 
files 

800 
"Gcd/greatest_common_divisor/g_c_d.fdl" 

801 
"Gcd/greatest_common_divisor/g_c_d.rls" 

802 
"Gcd/greatest_common_divisor/g_c_d.siv" 

803 
"Liseq/liseq/liseq_length.fdl" 

804 
"Liseq/liseq/liseq_length.rls" 

805 
"Liseq/liseq/liseq_length.siv" 

806 
"RIPEMD160/rmd/f.fdl" 

807 
"RIPEMD160/rmd/f.rls" 

808 
"RIPEMD160/rmd/f.siv" 

809 
"RIPEMD160/rmd/hash.fdl" 

810 
"RIPEMD160/rmd/hash.rls" 

811 
"RIPEMD160/rmd/hash.siv" 

812 
"RIPEMD160/rmd/k_l.fdl" 

813 
"RIPEMD160/rmd/k_l.rls" 

814 
"RIPEMD160/rmd/k_l.siv" 

815 
"RIPEMD160/rmd/k_r.fdl" 

816 
"RIPEMD160/rmd/k_r.rls" 

817 
"RIPEMD160/rmd/k_r.siv" 

818 
"RIPEMD160/rmd/r_l.fdl" 

819 
"RIPEMD160/rmd/r_l.rls" 

820 
"RIPEMD160/rmd/r_l.siv" 

821 
"RIPEMD160/rmd/round.fdl" 

822 
"RIPEMD160/rmd/round.rls" 

823 
"RIPEMD160/rmd/round.siv" 

824 
"RIPEMD160/rmd/r_r.fdl" 

825 
"RIPEMD160/rmd/r_r.rls" 

826 
"RIPEMD160/rmd/r_r.siv" 

827 
"RIPEMD160/rmd/s_l.fdl" 

828 
"RIPEMD160/rmd/s_l.rls" 

829 
"RIPEMD160/rmd/s_l.siv" 

830 
"RIPEMD160/rmd/s_r.fdl" 

831 
"RIPEMD160/rmd/s_r.rls" 

832 
"RIPEMD160/rmd/s_r.siv" 

833 

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

834 
session "HOLSPARKManual" in "SPARK/Manual" = "HOLSPARK" + 
48486  835 
options [show_question_marks = false] 
48481  836 
theories 
837 
Example_Verification 

838 
VC_Principles 

839 
Reference 

840 
Complex_Types 

841 
files 

842 
"complex_types_app/initialize.fdl" 

843 
"complex_types_app/initialize.rls" 

844 
"complex_types_app/initialize.siv" 

845 
"document/complex_types.ads" 

846 
"document/complex_types_app.adb" 

847 
"document/complex_types_app.ads" 

848 
"document/Gcd.adb" 

849 
"document/Gcd.ads" 

850 
"document/intro.tex" 

851 
"document/loop_invariant.adb" 

852 
"document/loop_invariant.ads" 

853 
"document/root.bib" 

854 
"document/root.tex" 

855 
"document/Simple_Gcd.adb" 

856 
"document/Simple_Gcd.ads" 

857 
"loop_invariant/proc1.fdl" 

858 
"loop_invariant/proc1.rls" 

859 
"loop_invariant/proc1.siv" 

860 
"loop_invariant/proc2.fdl" 

861 
"loop_invariant/proc2.rls" 

862 
"loop_invariant/proc2.siv" 

863 
"simple_greatest_common_divisor/g_c_d.fdl" 

864 
"simple_greatest_common_divisor/g_c_d.rls" 

865 
"simple_greatest_common_divisor/g_c_d.siv" 

866 

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

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

868 
options [document = false] 
48481  869 
theories MutabelleExtra 
870 

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

871 
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

872 
options [document = false] 
48588  873 
theories 
48690  874 
Quickcheck_Examples 
875 
(* FIXME 

876 
Quickcheck_Lattice_Examples 

877 
Completeness 

878 
Quickcheck_Interfaces 

879 
Hotel_Example *) 

48598  880 
theories [condition = ISABELLE_GHC] 
881 
Quickcheck_Narrowing_Examples 

48588  882 

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

883 
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

884 
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

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

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

887 
Needham_Schroeder_Guided_Attacker_Example 
48690  888 
Needham_Schroeder_Unguided_Attacker_Example 
48481  889 

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

890 
session "HOLQuotient_Examples" in Quotient_Examples = HOL + 
48481  891 
description {* 
892 
Author: Cezary Kaliszyk and Christian Urban 

893 
*} 

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

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

897 
FSet 

898 
Quotient_Int 

899 
Quotient_Message 

900 
Lift_FSet 

901 
Lift_Set 

902 
Lift_Fun 

903 
Quotient_Rat 

904 
Lift_DList 

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

905 
Int_Pow 
48481  906 

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

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

908 
options [document = false] 
48690  909 
theories 
48481  910 
Examples 
911 
Predicate_Compile_Tests 

48690  912 
(* FIXME 
913 
Predicate_Compile_Quickcheck_Examples  should be added again soon (since 21Oct2010) *) 

48481  914 
Specialisation_Examples 
48690  915 
(* FIXME since 21Jul2011 
916 
Hotel_Example_Small_Generator 

917 
IMP_1 

918 
IMP_2 

919 
IMP_3 

920 
IMP_4 *) 

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

922 
Code_Prolog_Examples 

923 
Context_Free_Grammar_Example 

924 
Hotel_Example_Prolog 

925 
Lambda_Example 

926 
List_Examples 

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

928 
Reg_Exp_Example 

48481  929 

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

930 
session HOLCF (main) in HOLCF = HOL + 
48338  931 
description {* 
932 
Author: Franz Regensburger 

933 
Author: Brian Huffman 

934 

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

936 
*} 

937 
options [document_graph] 

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

938 
theories [document = false] 
48338  939 
"~~/src/HOL/Library/Nat_Bijection" 
940 
"~~/src/HOL/Library/Countable" 

48481  941 
theories 
942 
Plain_HOLCF 

943 
Fixrec 

944 
HOLCF 

945 
files "document/root.tex" 

946 

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

947 
session "HOLCFTutorial" in "HOLCF/Tutorial" = HOLCF + 
48481  948 
theories 
949 
Domain_ex 

950 
Fixrec_ex 

951 
New_Domain 

952 
files "document/root.tex" 

953 

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

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

955 
options [document = false] 
48481  956 
theories HOLCF_Library 
957 

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

958 
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

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

960 
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

961 

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

962 
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

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

964 
options [document = false] 
48481  965 
theories HoareEx 
48338  966 
files "document/root.tex" 
967 

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

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

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

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

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

972 
options [document = false] 
48481  973 
theories 
974 
Dnat 

975 
Dagstuhl 

976 
Focus_ex 

977 
Fix2 

978 
Hoare 

979 
Concurrency_Monad 

980 
Loop 

981 
Powerdomain_ex 

982 
Domain_Proofs 

983 
Letrec 

984 
Pattern_Match 

985 

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

986 
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

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

988 
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

989 

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

990 
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

991 

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

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

993 
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

994 

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

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

996 
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

997 

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

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

999 
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

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

1001 
options [document = false] 
48481  1002 
theories 
1003 
Fstreams 

1004 
FOCUS 

1005 
Buffer_adm 

1006 

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

1007 
session IOA in "HOLCF/IOA" = HOLCF + 
48481  1008 
description {* 
1009 
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

1010 
Copyright 1997 TU München 
48481  1011 

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

1012 
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

1013 

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

1014 
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

1015 
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

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

1018 
options [document = false] 
48481  1019 
theories "meta_theory/Abstraction" 
1020 

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

1021 
session "IOAABP" in "HOLCF/IOA/ABP" = IOA + 
48481  1022 
description {* 
1023 
Author: Olaf Mueller 

1024 

1025 
The Alternating Bit Protocol performed in I/OAutomata. 

1026 
*} 

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

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

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

1030 
session "IOANTP" in "HOLCF/IOA/NTP" = IOA + 
48481  1031 
description {* 
1032 
Author: Tobias Nipkow & Konrad Slind 

1033 

1034 
A network transmission protocol, performed in the 

1035 
I/O automata formalization by Olaf Mueller. 

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 "IOAStorage" in "HOLCF/IOA/Storage" = IOA + 
48481  1041 
description {* 
1042 
Author: Olaf Mueller 

1043 

1044 
Memory storage case study. 

1045 
*} 

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

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

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

1049 
session "IOAex" in "HOLCF/IOA/ex" = IOA + 
48481  1050 
description {* 
1051 
Author: Olaf Mueller 

1052 
*} 

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

1053 
options [document = false] 
48481  1054 
theories 
1055 
TrivEx 

1056 
TrivEx2 

1057 

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

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

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

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

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

1062 
options [document = false] 
48635  1063 
theories [condition = ISABELLE_FULL_TEST, timing] 
48481  1064 
Brackin 
1065 
Instructions 

1066 
SML 

1067 
Verilog 

1068 

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

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

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

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

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

1073 
options [document = false] 
48635  1074 
theories [condition = ISABELLE_FULL_TEST, timing] 
48481  1075 
Record_Benchmark 
1076 