author  wenzelm 
Mon, 24 Apr 2017 23:10:01 +0200  
changeset 65576  8376f83f9094 
parent 65574  10f4a17e5928 
child 65678  aaba2e0c247c 
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 
*} 
65374  7 
theories 
8 
Main (global) 

9 
Complex_Main (global) 

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

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

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

12 
"Tools/Quickcheck/PNF_Narrowing_Engine.hs" 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

13 
document_files 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

14 
"root.bib" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

15 
"root.tex" 
48338  16 

63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset

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

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

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

20 
*} 
65456
31e8a86971a8
explicit theory qualifier for session "HOLProofs": its theory name space overlaps with session "HOL", even for further imports;
wenzelm
parents:
65448
diff
changeset

21 
options [document = false, theory_qualifier = "HOL", 
31e8a86971a8
explicit theory qualifier for session "HOLProofs": its theory name space overlaps with session "HOL", even for further imports;
wenzelm
parents:
65448
diff
changeset

22 
quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0] 
65543  23 
sessions 
24 
"HOLLibrary" 

65530
09c00a304c00
include imports that morally belong to Main and are used in HOLProofs applications;
wenzelm
parents:
65509
diff
changeset

25 
theories 
09c00a304c00
include imports that morally belong to Main and are used in HOLProofs applications;
wenzelm
parents:
65509
diff
changeset

26 
"HOLLibrary.Old_Datatype" 
48901
5e0455e29339
more basic file dependencies  no load command here;
wenzelm
parents:
48765
diff
changeset

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

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

29 
"Tools/Quickcheck/PNF_Narrowing_Engine.hs" 
48338  30 

63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset

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

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

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

34 
*} 
48481  35 
theories 
36 
Library 

64588  37 
(*conflicting type class instantiations and dependent applications*) 
38 
Finite_Lattice 

39 
List_lexord 

63763
0f61ea70d384
clarified session: use all theories in directory HOL/Library;
wenzelm
parents:
63731
diff
changeset

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

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

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

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

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

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

47 
Code_Char 
55447  48 
Code_Prolog 
48481  49 
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

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

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

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

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

54 
RBT_Set 
64588  55 
(*prototypic tools*) 
56 
Predicate_Compile_Quickcheck 

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

57 
(*legacy tools*) 
58372
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOLProofs' because of the inductive realizer)
blanchet
parents:
58371
diff
changeset

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

59 
Old_Recdef 
64588  60 
Refute 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

61 
document_files "root.bib" "root.tex" 
48481  62 

65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset

63 
session "HOLAnalysis" (main timing) in Analysis = "HOLComputational_Algebra" + 
65375  64 
theories 
65462
db1827610513
less global theories  conflict with AFP entries;
wenzelm
parents:
65456
diff
changeset

65 
Analysis 
65375  66 
document_files 
67 
"root.tex" 

68 

69 
session "HOLAnalysisex" in "Analysis/ex" = "HOLAnalysis" + 

70 
theories 

71 
Approximations 

72 
Circle_Area 

73 

65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset

74 
session "HOLComputational_Algebra" in "Computational_Algebra" = "HOLLibrary" + 
65417  75 
theories 
76 
Computational_Algebra 

77 
(*conflicting type class instantiations and dependent applications*) 

78 
Field_as_Ring 

79 
Polynomial_Factorial 

80 

65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset

81 
session "HOLHahn_Banach" in Hahn_Banach = "HOLLibrary" + 
48481  82 
description {* 
83 
Author: Gertrud Bauer, TU Munich 

84 

85 
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

86 

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

87 
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

88 
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

89 
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

90 
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

91 

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

92 
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

93 
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

94 

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

95 
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

96 
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

97 
continous linearform on the whole vectorspace. 
48481  98 
*} 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

99 
sessions 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

100 
"HOLAnalysis" 
65543  101 
theories 
102 
Hahn_Banach 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

103 
document_files "root.bib" "root.tex" 
48481  104 

65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset

105 
session "HOLInduct" in Induct = "HOLLibrary" + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

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

107 
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

108 

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

109 
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

110 
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

111 

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

112 
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

113 
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

114 

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

115 
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

116 
(see 
58372
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOLProofs' because of the inductive realizer)
blanchet
parents:
58371
diff
changeset

117 
http://www.cl.cam.ac.uk/Research/Reports/TR312lcpsetII.ps.gz). 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

118 

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

119 
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

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

121 
*} 
58372
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOLProofs' because of the inductive realizer)
blanchet
parents:
58371
diff
changeset

122 
theories [document = false] 
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOLProofs' because of the inductive realizer)
blanchet
parents:
58371
diff
changeset

123 
"~~/src/HOL/Library/Old_Datatype" 
48481  124 
theories [quick_and_dirty] 
125 
Common_Patterns 

126 
theories 

61935  127 
Nested_Datatype 
48481  128 
QuoDataType 
129 
QuoNestedDataType 

130 
Term 

131 
SList 

132 
ABexp 

65562
f9753d949afc
renamed theory to avoid conflict with loaded theory "Tree" from HOLLibrary;
wenzelm
parents:
65552
diff
changeset

133 
Infinitely_Branching_Tree 
48481  134 
Ordinals 
135 
Sigma_Algebra 

136 
Comb 

137 
PropLog 

138 
Com 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

139 
document_files "root.tex" 
48481  140 

65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

141 
session "HOLIMP" (timing) in IMP = "HOLLibrary" + 
59446  142 
options [document_variants = document] 
48481  143 
theories [document = false] 
144 
"~~/src/HOL/Library/While_Combinator" 

145 
"~~/src/HOL/Library/Char_ord" 

146 
"~~/src/HOL/Library/List_lexord" 

51625  147 
"~~/src/HOL/Library/Quotient_List" 
148 
"~~/src/HOL/Library/Extended" 

48481  149 
theories 
150 
BExp 

151 
ASM 

50050  152 
Finite_Reachable 
52394  153 
Denotational 
52400  154 
Compiler2 
48481  155 
Poly_Types 
156 
Sec_Typing 

157 
Sec_TypingT 

52726  158 
Def_Init_Big 
159 
Def_Init_Small 

160 
Fold 

48481  161 
Live 
162 
Live_True 

163 
Hoare_Examples 

63538
d7b5e2a222c2
added new vcg based on existentially quantified whilerule
nipkow
parents:
63537
diff
changeset

164 
Hoare_Sound_Complete 
52269  165 
VCG 
52282  166 
Hoare_Total 
63538
d7b5e2a222c2
added new vcg based on existentially quantified whilerule
nipkow
parents:
63537
diff
changeset

167 
VCG_Total_EX 
48481  168 
Collecting1 
48765
fb1ed5230abc
special code with lists no longer necessary, use sets
nipkow
parents:
48738
diff
changeset

169 
Collecting_Examples 
48481  170 
Abs_Int_Tests 
171 
Abs_Int1_parity 

172 
Abs_Int1_const 

173 
Abs_Int3 

174 
Procs_Dyn_Vars_Dyn 

175 
Procs_Stat_Vars_Dyn 

176 
Procs_Stat_Vars_Stat 

177 
C_like 

178 
OO 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

179 
document_files "root.bib" "root.tex" 
48481  180 

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

181 
session "HOLIMPP" in IMPP = HOL + 
48481  182 
description {* 
183 
Author: David von Oheimb 

184 
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

185 

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

186 
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

187 

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

188 
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

189 
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

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

192 
options [document = false] 
48481  193 
theories EvenOdd 
194 

63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset

195 
session "HOLData_Structures" (timing) in Data_Structures = HOL + 
61203  196 
options [document_variants = document] 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

197 
sessions 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

198 
"HOLNumber_Theory" 
61203  199 
theories [document = false] 
65538  200 
Less_False 
62706  201 
"~~/src/HOL/Library/Multiset" 
64323  202 
"~~/src/HOL/Number_Theory/Fib" 
61203  203 
theories 
63829  204 
Balance 
61203  205 
Tree_Map 
61232  206 
AVL_Map 
61224  207 
RBT_Map 
61469
cd82b1023932
added 23 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
61368
diff
changeset

208 
Tree23_Map 
61514  209 
Tree234_Map 
61789  210 
Brother12_Map 
62130  211 
AA_Map 
61525  212 
Splay_Map 
62706  213 
Leftist_Heap 
61224  214 
document_files "root.tex" "root.bib" 
61203  215 

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

216 
session "HOLImport" in Import = HOL + 
48481  217 
theories HOL_Light_Maps 
218 
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 

219 

65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset

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

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

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

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

224 
*} 
65543  225 
sessions 
226 
"HOLAlgebra" 

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

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

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

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

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

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

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

233 
Number_Theory 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

234 
document_files 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

235 
"root.tex" 
48481  236 

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

237 
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

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

239 
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

240 
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

241 
*} 
48481  242 
theories Hoare 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

243 
document_files "root.bib" "root.tex" 
48481  244 

63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset

245 
session "HOLHoare_Parallel" (timing) 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

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

247 
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

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

249 
*} 
48481  250 
theories Hoare_Parallel 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

251 
document_files "root.bib" "root.tex" 
48481  252 

65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset

253 
session "HOLCodegenerator_Test" in Codegenerator_Test = "HOLNumber_Theory" + 
62354  254 
options [document = false, browser_info = false] 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

255 
sessions 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

256 
"HOLData_Structures" 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

257 
"HOLex" 
51422
821a70e29e0b
proper formatting, to facilitate linebased diff;
wenzelm
parents:
51421
diff
changeset

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

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

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

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

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

263 
Generate_Pretty_Char 
64582
3d20ded18f14
unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
wenzelm
parents:
64569
diff
changeset

264 
Code_Test_PolyML 
3d20ded18f14
unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
wenzelm
parents:
64569
diff
changeset

265 
Code_Test_Scala 
62354  266 
theories [condition = "ISABELLE_GHC"] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

267 
Code_Test_GHC 
62354  268 
theories [condition = "ISABELLE_MLTON"] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

269 
Code_Test_MLton 
62354  270 
theories [condition = "ISABELLE_OCAMLC"] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

271 
Code_Test_OCaml 
62354  272 
theories [condition = "ISABELLE_SMLNJ"] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

273 
Code_Test_SMLNJ 
48481  274 

65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

275 
session "HOLMetis_Examples" (timing) in Metis_Examples = "HOLLibrary" + 
48481  276 
description {* 
277 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

278 
Author: Jasmin Blanchette, TU Muenchen 

279 

280 
Testing Metis and Sledgehammer. 

281 
*} 

58423  282 
options [document = false] 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

283 
sessions 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

284 
"HOLDecision_Procs" 
48481  285 
theories 
286 
Abstraction 

287 
Big_O 

288 
Binary_Tree 

289 
Clausification 

290 
Message 

291 
Proxies 

292 
Tarski 

293 
Trans_Closure 

294 
Sets 

295 

65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

296 
session "HOLNitpick_Examples" in Nitpick_Examples = "HOLLibrary" + 
48481  297 
description {* 
298 
Author: Jasmin Blanchette, TU Muenchen 

299 
Copyright 2009 

300 
*} 

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

301 
options [document = false] 
48481  302 
theories [quick_and_dirty] Nitpick_Examples 
303 

64389  304 
session "HOLNunchaku" in Nunchaku = HOL + 
305 
description {* 

306 
Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII 

307 
Copyright 2015, 2016 

308 

309 
Nunchaku: Yet another counterexample generator for Isabelle/HOL. 

310 
*} 

311 
options [document = false] 

312 
theories Nunchaku 

313 

65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset

314 
session "HOLAlgebra" (main timing) in Algebra = "HOLComputational_Algebra" + 
48481  315 
description {* 
316 
Author: Clemens Ballarin, started 24 September 1999 

317 

318 
The Isabelle Algebraic Library. 

319 
*} 

320 
theories [document = false] 

321 
(* Preliminaries from set and number theory *) 

322 
"~~/src/HOL/Library/FuncSet" 

65417  323 
"~~/src/HOL/Computational_Algebra/Primes" 
48481  324 
"~~/src/HOL/Library/Permutation" 
325 
theories 

65099
30d0b2f1df76
KnasterTarski fixed point theorem and Galois Connections.
ballarin
parents:
65050
diff
changeset

326 
(* Orders and Lattices *) 
30d0b2f1df76
KnasterTarski fixed point theorem and Galois Connections.
ballarin
parents:
65050
diff
changeset

327 
Galois_Connection (* KnasterTarski theorem and Galois connections *) 
30d0b2f1df76
KnasterTarski fixed point theorem and Galois Connections.
ballarin
parents:
65050
diff
changeset

328 

48481  329 
(* Groups *) 
330 
FiniteProduct (* Product operator for commutative groups *) 

331 
Sylow (* Sylow's theorem *) 

332 
Bij (* Automorphism Groups *) 

65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65382
diff
changeset

333 
More_Group 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65382
diff
changeset

334 
More_Finite_Product 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65382
diff
changeset

335 
Multiplicative_Group 
48481  336 

337 
(* Rings *) 

338 
Divisibility (* Rings *) 

339 
IntRing (* Ideals and residue classes *) 

340 
UnivPoly (* Polynomials *) 

65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65382
diff
changeset

341 
More_Ring 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

342 
document_files "root.bib" "root.tex" 
48481  343 

65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

344 
session "HOLAuth" (timing) in Auth = "HOLLibrary" + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

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

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

347 
*} 
48481  348 
theories 
349 
Auth_Shared 

350 
Auth_Public 

351 
"Smartcard/Auth_Smartcard" 

352 
"Guard/Auth_Guard_Shared" 

353 
"Guard/Auth_Guard_Public" 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

354 
document_files "root.tex" 
48481  355 

63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset

356 
session "HOLUNITY" (timing) in UNITY = "HOLAuth" + 
48481  357 
description {* 
358 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

359 
Copyright 1998 University of Cambridge 

360 

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

361 
Verifying security protocols using Chandy and Misra's UNITY formalism. 
48481  362 
*} 
363 
theories 

364 
(*Basic metatheory*) 

65538  365 
UNITY_Main 
48481  366 

367 
(*Simple examples: no composition*) 

368 
"Simple/Deadlock" 

369 
"Simple/Common" 

370 
"Simple/Network" 

371 
"Simple/Token" 

372 
"Simple/Channel" 

373 
"Simple/Lift" 

374 
"Simple/Mutex" 

375 
"Simple/Reach" 

376 
"Simple/Reachability" 

377 

378 
(*Verifying security protocols using UNITY*) 

379 
"Simple/NSP_Bad" 

380 

381 
(*Example of composition*) 

382 
"Comp/Handshake" 

383 

384 
(*Universal properties examples*) 

385 
"Comp/Counter" 

386 
"Comp/Counterc" 

387 
"Comp/Priority" 

388 

389 
"Comp/TimerArray" 

390 
"Comp/Progress" 

391 

392 
"Comp/Alloc" 

393 
"Comp/AllocImpl" 

394 
"Comp/Client" 

395 

396 
(*obsolete*) 

65538  397 
ELT 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

398 
document_files "root.tex" 
48481  399 

65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

400 
session "HOLUnix" in Unix = "HOLLibrary" + 
48481  401 
options [print_mode = "no_brackets,no_type_brackets"] 
402 
theories Unix 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

403 
document_files "root.bib" "root.tex" 
48481  404 

65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

405 
session "HOLZF" in ZF = "HOLLibrary" + 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

406 
theories 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

407 
MainZF 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

408 
Games 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

409 
document_files "root.tex" 
48481  410 

65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset

411 
session "HOLImperative_HOL" in Imperative_HOL = "HOLLibrary" + 
59446  412 
options [print_mode = "iff,no_brackets"] 
48481  413 
theories [document = false] 
414 
"~~/src/HOL/Library/Countable" 

415 
"~~/src/HOL/Library/Monad_Syntax" 

416 
"~~/src/HOL/Library/LaTeXsugar" 

417 
theories Imperative_HOL_ex 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

418 
document_files "root.bib" "root.tex" 
48481  419 

65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset

420 
session "HOLDecision_Procs" (timing) in Decision_Procs = "HOLAlgebra" + 
51544  421 
description {* 
422 
Various decision procedures, typically involving reflection. 

423 
*} 

62354  424 
options [document = false] 
65543  425 
theories 
426 
Decision_Procs 

48481  427 

63000
d0dfdd413a7f
remove "slow" session tags
Lars Hupel <lars.hupel@mytum.de>
parents:
62999
diff
changeset

428 
session "HOLProofsex" in "Proofs/ex" = "HOLProofs" + 
64597
1c252d8b6ca6
test parallel proof terms in this small session (somewhat slow for bigger applications);
wenzelm
parents:
64591
diff
changeset

429 
options [document = false] 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

430 
sessions 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

431 
"HOLIsar_Examples" 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
52400
diff
changeset

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

433 
Hilbert_Classical 
62363
7b5468422352
moved examples to avoid dependency on bulky HOLProofs session, e.g. relevant for "isabelle makedist";
wenzelm
parents:
62357
diff
changeset

434 
Proof_Terms 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
52400
diff
changeset

435 
XML_Data 
48481  436 

63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset

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

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

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

440 
*} 
62354  441 
options [parallel_proofs = 0, quick_and_dirty = false] 
65543  442 
sessions 
443 
"HOLLibrary" 

444 
"HOLComputational_Algebra" 

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

446 
"~~/src/HOL/Library/Code_Target_Numeral" 
48481  447 
"~~/src/HOL/Library/Monad_Syntax" 
65417  448 
"~~/src/HOL/Computational_Algebra/Primes" 
48481  449 
"~~/src/HOL/Library/State_Monad" 
450 
theories 

451 
Greatest_Common_Divisor 

452 
Warshall 

453 
Higman_Extraction 

454 
Pigeonhole 

455 
Euclid 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

456 
document_files "root.bib" "root.tex" 
48481  457 

63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset

458 
session "HOLProofsLambda" (timing) 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

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

460 
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

461 

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

462 
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

463 
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

464 

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

465 
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

466 
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

467 
*} 
62354  468 
options [print_mode = "no_brackets", 
62242
a4e6ea45f416
guard sessions that no longer work with SML/NJ  memory problems;
wenzelm
parents:
62168
diff
changeset

469 
parallel_proofs = 0, quick_and_dirty = false] 
65543  470 
sessions 
471 
"HOLLibrary" 

48481  472 
theories 
473 
Eta 

474 
StrongNorm 

475 
Standardization 

476 
WeakNorm 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

477 
document_files "root.bib" "root.tex" 
48481  478 

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

479 
session "HOLProlog" in Prolog = HOL + 
48481  480 
description {* 
481 
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

482 

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

483 
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

484 

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

485 
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

486 
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

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

489 
options [document = false] 
48481  490 
theories Test Type 
491 

65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset

492 
session "HOLMicroJava" (timing) in MicroJava = "HOLLibrary" + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

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

494 
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

495 
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

496 
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

497 
*} 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

498 
sessions 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

499 
"HOLEisbach" 
59446  500 
theories [document = false] 
501 
"~~/src/HOL/Library/While_Combinator" 

502 
theories 

503 
MicroJava 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

504 
document_files 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

505 
"introduction.tex" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

506 
"root.bib" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

507 
"root.tex" 
48481  508 

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

509 
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

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

511 
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

512 
*} 
48481  513 
theories Example 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

514 
document_files "root.bib" "root.tex" 
48481  515 

65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

516 
session "HOLBali" (timing) in Bali = "HOLLibrary" + 
48481  517 
theories 
518 
AxExample 

519 
AxSound 

520 
AxCompl 

521 
Trans 

60751  522 
TypeSafe 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

523 
document_files "root.tex" 
48481  524 

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

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

527 
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

528 
Copyright 19941996 TU Muenchen 
48481  529 

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

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

531 
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

532 
proofs of two communication protocols which formerly have been here. 
48481  533 

534 
@inproceedings{NipkowSlindIOA, 

535 
author={Tobias Nipkow and Konrad Slind}, 

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

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

538 
publisher=Springer, 

539 
series=LNCS, 

540 
note={To appear}} 

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

542 

543 
and 

544 

545 
@inproceedings{MuellerNipkow, 

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

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

548 
booktitle={Proc.\ TACAS Workshop}, 

549 
organization={Aarhus University, BRICS report}, 

550 
year=1995} 

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

552 
*} 

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

553 
options [document = false] 
48481  554 
theories Solve 
555 

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

556 
session "HOLLattice" in Lattice = HOL + 
48481  557 
description {* 
558 
Author: Markus Wenzel, TU Muenchen 

559 

560 
Basic theory of lattices and orders. 

561 
*} 

562 
theories CompleteLattice 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

563 
document_files "root.tex" 
48481  564 

65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset

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

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

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

568 
*} 
65548  569 
options [document = false] 
65543  570 
sessions 
571 
"HOLNumber_Theory" 

65548  572 
theories 
57507  573 
Adhoc_Overloading_Examples 
48481  574 
Antiquote 
65549  575 
Argo_Examples 
576 
Arith_Examples 

577 
Ballot 

578 
BinEx 

579 
Birthday_Paradox 

580 
Bubblesort 

581 
CTL 

582 
Cartouche_Examples 

65563  583 
Case_Product 
65549  584 
Chinese 
585 
Classical 

586 
Code_Binary_Nat_examples 

587 
Code_Timing 

588 
Coercion_Examples 

589 
Coherent 

590 
Commands 

591 
Computations 

59190
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
59162
diff
changeset

592 
Cubic_Quartic 
65549  593 
Dedekind_Real 
594 
Erdoes_Szekeres 

595 
Eval_Examples 

596 
Executable_Relation 

597 
Execute_Choice 

598 
Functions 

599 
Gauge_Integration 

600 
Groebner_Examples 

601 
Guess 

602 
HarmonicSeries 

603 
Hebrew 

604 
Hex_Bin_Examples 

605 
IArray_Examples 

606 
Iff_Oracle 

607 
Induction_Schema 

48481  608 
Intuitionistic 
65549  609 
Lagrange 
610 
List_to_Set_Comprehension_Examples 

611 
LocaleTest2 

612 
ML 

48481  613 
MergeSort 
65549  614 
MonoidGroup 
615 
Multiquote 

616 
NatSum 

617 
Normalization_by_Evaluation 

618 
PER 

619 
Parallel_Example 

620 
Peano_Axioms 

621 
Perm_Fragments 

622 
PresburgerEx 

48481  623 
Primrec 
65549  624 
Pythagoras 
625 
Quicksort 

626 
Records 

627 
Reflection_Examples 

628 
Refute_Examples 

629 
Rewrite_Examples 

630 
SAT_Examples 

631 
SOS 

632 
SOS_Cert 

633 
Seq 

634 
Serbian 

635 
Set_Comprehension_Pointfree_Examples 

48481  636 
Set_Theory 
65549  637 
Simproc_Tests 
638 
Simps_Case_Conv_Examples 

48481  639 
Sqrt 
640 
Sqrt_Script 

65549  641 
Sudoku 
642 
Sum_of_Powers 

643 
Tarski 

644 
Termination 

645 
ThreeDivides 

61368  646 
Transfer_Debug 
48481  647 
Transfer_Ex 
648 
Transfer_Int_Nat 

56922  649 
Transitive_Closure_Table_Ex 
65549  650 
Tree23 
651 
Unification 

652 
While_Combinator_Example 

64015
c9f3a94cb825
proof of concept for algebraically founded word types
haftmann
parents:
63980
diff
changeset

653 
Word_Type 
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
64959
diff
changeset

654 
veriT_Preprocessing 
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

655 
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

656 
Meson_Test 
48481  657 

65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset

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

659 
description {* 
61935  660 
Miscellaneous Isabelle/Isar examples. 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

661 
*} 
61939  662 
options [quick_and_dirty] 
48481  663 
theories [document = false] 
664 
"~~/src/HOL/Library/Lattice_Syntax" 

65417  665 
"../Computational_Algebra/Primes" 
48481  666 
theories 
61939  667 
Knaster_Tarski 
668 
Peirce 

669 
Drinker 

48481  670 
Cantor 
61939  671 
Structured_Statements 
672 
Basic_Logic 

48481  673 
Expr_Compiler 
674 
Fibonacci 

675 
Group 

676 
Group_Context 

677 
Group_Notepad 

678 
Hoare_Ex 

679 
Mutilated_Checkerboard 

680 
Puzzle 

681 
Summation 

61935  682 
First_Order_Logic 
683 
Higher_Order_Logic 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

684 
document_files 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

685 
"root.bib" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

686 
"root.tex" 
48481  687 

60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset

688 
session "HOLEisbach" in Eisbach = HOL + 
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset

689 
description {* 
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset

690 
The Eisbach proof method language and "match" method. 
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset

691 
*} 
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset

692 
theories 
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset

693 
Eisbach 
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset

694 
Tests 
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset

695 
Examples 
62168
e97452d79102
Eisbach works for other objectlogics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62155
diff
changeset

696 
Examples_FOL 
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset

697 

65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset

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

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

700 
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

701 
*} 
65543  702 
theories [document = false] 
703 
"~~/src/HOL/Library/Nat_Bijection" 

704 
theories 

705 
SET_Protocol 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

706 
document_files "root.tex" 
48481  707 

65569
3cb6f3281ef1
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65563
diff
changeset

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

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

710 
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

711 
*} 
48481  712 
theories Cplex 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

713 
document_files "root.tex" 
48481  714 

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

715 
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

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

717 
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

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

719 
options [document = false] 
48481  720 
theories TLA 
721 

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

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

723 
options [document = false] 
48481  724 
theories Inc 
725 

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

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

727 
options [document = false] 
48481  728 
theories DBuffer 
729 

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

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

731 
options [document = false] 
48481  732 
theories MemoryImplementation 
733 

65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

734 
session "HOLTPTP" in TPTP = "HOLLibrary" + 
48481  735 
description {* 
736 
Author: Jasmin Blanchette, TU Muenchen 

737 
Author: Nik Sultana, University of Cambridge 

738 
Copyright 2011 

739 

740 
TPTPrelated extensions. 

741 
*} 

62354  742 
options [document = false] 
48481  743 
theories 
744 
ATP_Theory_Export 

745 
MaSh_Eval 

746 
TPTP_Interpret 

747 
THF_Arith 

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

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

749 
theories 
48481  750 
ATP_Problem_Import 
751 

65382  752 
session "HOLProbability" (main timing) in "Probability" = "HOLAnalysis" + 
48481  753 
theories [document = false] 
754 
"~~/src/HOL/Library/Countable" 

755 
"~~/src/HOL/Library/Permutation" 

56994  756 
"~~/src/HOL/Library/Order_Continuity" 
757 
"~~/src/HOL/Library/Diagonal_Subsequence" 

63885
a6cd18af8bf9
new type for finite maps; use it in HOLProbability
Lars Hupel <lars.hupel@mytum.de>
parents:
63829
diff
changeset

758 
"~~/src/HOL/Library/Finite_Map" 
48481  759 
theories 
65382  760 
Probability (global) 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

761 
document_files "root.tex" 
48481  762 

63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset

763 
session "HOLProbabilityex" (timing) in "Probability/ex" = "HOLProbability" + 
61946
844881193616
put example into separate session, to restrict precious session image to library theories
haftmann
parents:
61939
diff
changeset

764 
theories 
65538  765 
Dining_Cryptographers 
766 
Koepf_Duermuth_Countermeasure 

767 
Measure_Not_CCC 

61946
844881193616
put example into separate session, to restrict precious session image to library theories
haftmann
parents:
61939
diff
changeset

768 

59898
81c70bdbd908
clarified "main" group, e.g. relevant for Isabelle/jEdit menu;
wenzelm
parents:
59810
diff
changeset

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

770 
options [document = false] 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

771 
sessions 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

772 
"HOLLibrary" 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

773 
theories 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

774 
Nominal 
48481  775 

63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset

776 
session "HOLNominalExamples" (timing) in "Nominal/Examples" = "HOLNominal" + 
62354  777 
options [document = false] 
58329
a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents:
58313
diff
changeset

778 
theories 
59162
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

779 
Class3 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

780 
CK_Machine 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

781 
Compile 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

782 
Contexts 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

783 
Crary 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

784 
CR_Takahashi 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

785 
CR 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

786 
Fsub 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

787 
Height 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

788 
Lambda_mu 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

789 
Lam_Funs 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

790 
LocalWeakening 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

791 
Pattern 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

792 
SN 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

793 
SOS 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

794 
Standardization 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

795 
Support 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

796 
Type_Preservation 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

797 
Weakening 
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset

798 
W 
58329
a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents:
58313
diff
changeset

799 
theories [quick_and_dirty] 
a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents:
58313
diff
changeset

800 
VC_Condition 
48481  801 

65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

802 
session "HOLCardinals" (timing) in Cardinals = "HOLLibrary" + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

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

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

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

806 
options [document = false] 
59747  807 
theories 
808 
Cardinals 

809 
Bounded_Set 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

810 
document_files 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

811 
"intro.tex" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

812 
"root.tex" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

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

814 

65574
10f4a17e5928
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65573
diff
changeset

815 
session "HOLDatatype_Examples" (timing) in Datatype_Examples = "HOLLibrary" + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

816 
description {* 
62286
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build a" by default;
wenzelm
parents:
62285
diff
changeset

817 
(Co)datatype Examples. 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

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

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

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

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

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

824 
TreeFsetI 
49872  825 
"Derivation_Trees/Gram_Lang" 
65574
10f4a17e5928
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65573
diff
changeset

826 
"Derivation_Trees/Parallel_Composition" 
50517  827 
Koenig 
60921  828 
Lift_BNF 
61745  829 
Milner_Tofte 
54961  830 
Stream_Processor 
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset

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

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

835 

65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

836 
session "HOLCorec_Examples" (timing) in Corec_Examples = "HOLLibrary" + 
62694  837 
description {* 
838 
Corecursion Examples. 

839 
*} 

840 
options [document = false] 

841 
theories 

842 
LFilter 

62734  843 
Paper_Examples 
62694  844 
Stream_Processor 
62696  845 
"Tests/Simple_Nesting" 
64379
71f42dcaa1df
additional userspecified simp (naturality) rules used in friend_of_corec
traytel
parents:
64323
diff
changeset

846 
"Tests/Iterate_GPV" 
62696  847 
theories [quick_and_dirty] 
848 
"Tests/GPV_Bare_Bones" 

849 
"Tests/Merge_D" 

850 
"Tests/Merge_Poly" 

851 
"Tests/Misc_Mono" 

852 
"Tests/Misc_Poly" 

853 
"Tests/Small_Concrete" 

62725  854 
"Tests/Stream_Friends" 
62696  855 
"Tests/TLList_Friends" 
63190  856 
"Tests/Type_Class" 
62694  857 

63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset

858 
session "HOLWord" (main timing) in Word = HOL + 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

859 
sessions 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

860 
"HOLLibrary" 
65382  861 
theories 
65462
db1827610513
less global theories  conflict with AFP entries;
wenzelm
parents:
65456
diff
changeset

862 
Word 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

863 
document_files "root.bib" "root.tex" 
48481  864 

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

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

866 
options [document = false] 
48481  867 
theories WordExamples 
868 

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

869 
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

870 
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

871 
StateSpaceEx 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

872 
document_files "root.tex" 
48481  873 

65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset

874 
session "HOLNonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOLComputational_Algebra" + 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

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

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

877 
*} 
62479  878 
theories 
879 
Nonstandard_Analysis 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

880 
document_files "root.tex" 
48481  881 

63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset

882 
session "HOLNonstandard_AnalysisExamples" (timing) in "Nonstandard_Analysis/Examples" = "HOLNonstandard_Analysis" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

883 
options [document = false] 
65543  884 
theories 
885 
NSPrimes 

48481  886 

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

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

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

890 

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

891 
session "HOLMirabelleex" in "Mirabelle/ex" = "HOLMirabelle" + 
62354  892 
options [document = false, timeout = 60] 
49448
8a232a4e3fd8
reactivate HOLMirabelleex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
wenzelm
parents:
49439
diff
changeset

893 
theories Ex 
48481  894 

63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset

895 
session "HOLWordSMT_Examples" (timing) in SMT_Examples = "HOLWord" + 
62354  896 
options [document = false, quick_and_dirty] 
48481  897 
theories 
52722  898 
Boogie 
48481  899 
SMT_Examples 
900 
SMT_Word_Examples 

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

901 
SMT_Tests 
48481  902 
files 
58367
8af1e68d7e1a
renamed SMT certificate files, following 'SMT2' > 'SMT' renaming
blanchet
parents:
58351
diff
changeset

903 
"Boogie_Dijkstra.certs" 
8af1e68d7e1a
renamed SMT certificate files, following 'SMT2' > 'SMT' renaming
blanchet
parents:
58351
diff
changeset

904 
"Boogie_Max.certs" 
8af1e68d7e1a
renamed SMT certificate files, following 'SMT2' > 'SMT' renaming
blanchet
parents:
58351
diff
changeset

905 
"SMT_Examples.certs" 
8af1e68d7e1a
renamed SMT certificate files, following 'SMT2' > 'SMT' renaming
blanchet
parents:
58351
diff
changeset

906 
"SMT_Word_Examples.certs" 
8af1e68d7e1a
renamed SMT certificate files, following 'SMT2' > 'SMT' renaming
blanchet
parents:
58351
diff
changeset

907 
"VCC_Max.certs" 
48481  908 

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

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

910 
options [document = false] 
65382  911 
theories 
912 
SPARK (global) 

48481  913 

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

914 
session "HOLSPARKExamples" in "SPARK/Examples" = "HOLSPARK" + 
59810
e749a0f2f401
HOLSPARK .prv files are subject to system option spark_prv;
wenzelm
parents:
59777
diff
changeset

915 
options [document = false, spark_prv = false] 
48481  916 
theories 
917 
"Gcd/Greatest_Common_Divisor" 

918 

919 
"Liseq/Longest_Increasing_Subsequence" 

920 

921 
"RIPEMD160/F" 

922 
"RIPEMD160/Hash" 

923 
"RIPEMD160/K_L" 

924 
"RIPEMD160/K_R" 

925 
"RIPEMD160/R_L" 

926 
"RIPEMD160/Round" 

927 
"RIPEMD160/R_R" 

928 
"RIPEMD160/S_L" 

929 
"RIPEMD160/S_R" 

930 

931 
"Sqrt/Sqrt" 

932 
files 

933 
"Gcd/greatest_common_divisor/g_c_d.fdl" 

934 
"Gcd/greatest_common_divisor/g_c_d.rls" 

935 
"Gcd/greatest_common_divisor/g_c_d.siv" 

936 
"Liseq/liseq/liseq_length.fdl" 

937 
"Liseq/liseq/liseq_length.rls" 

938 
"Liseq/liseq/liseq_length.siv" 

939 
"RIPEMD160/rmd/f.fdl" 

940 
"RIPEMD160/rmd/f.rls" 

941 
"RIPEMD160/rmd/f.siv" 

942 
"RIPEMD160/rmd/hash.fdl" 

943 
"RIPEMD160/rmd/hash.rls" 

944 
"RIPEMD160/rmd/hash.siv" 

945 
"RIPEMD160/rmd/k_l.fdl" 

946 
"RIPEMD160/rmd/k_l.rls" 

947 
"RIPEMD160/rmd/k_l.siv" 

948 
"RIPEMD160/rmd/k_r.fdl" 

949 
"RIPEMD160/rmd/k_r.rls" 

950 
"RIPEMD160/rmd/k_r.siv" 

951 
"RIPEMD160/rmd/r_l.fdl" 

952 
"RIPEMD160/rmd/r_l.rls" 

953 
"RIPEMD160/rmd/r_l.siv" 

954 
"RIPEMD160/rmd/round.fdl" 

955 
"RIPEMD160/rmd/round.rls" 

956 
"RIPEMD160/rmd/round.siv" 

957 
"RIPEMD160/rmd/r_r.fdl" 

958 
"RIPEMD160/rmd/r_r.rls" 

959 
"RIPEMD160/rmd/r_r.siv" 

960 
"RIPEMD160/rmd/s_l.fdl" 

961 
"RIPEMD160/rmd/s_l.rls" 

962 
"RIPEMD160/rmd/s_l.siv" 

963 
"RIPEMD160/rmd/s_r.fdl" 

964 
"RIPEMD160/rmd/s_r.rls" 

965 
"RIPEMD160/rmd/s_r.siv" 

966 

65576  967 
session "HOLSPARKManual" in "SPARK/Manual" = "HOLSPARK" + 
59810
e749a0f2f401
HOLSPARK .prv files are subject to system option spark_prv;
wenzelm
parents:
59777
diff
changeset

968 
options [show_question_marks = false, spark_prv = false] 
48481  969 
theories 
970 
Example_Verification 

971 
VC_Principles 

972 
Reference 

973 
Complex_Types 

974 
files 

975 
"complex_types_app/initialize.fdl" 

976 
"complex_types_app/initialize.rls" 

977 
"complex_types_app/initialize.siv" 

978 
"loop_invariant/proc1.fdl" 

979 
"loop_invariant/proc1.rls" 

980 
"loop_invariant/proc1.siv" 

981 
"loop_invariant/proc2.fdl" 

982 
"loop_invariant/proc2.rls" 

983 
"loop_invariant/proc2.siv" 

984 
"simple_greatest_common_divisor/g_c_d.fdl" 

985 
"simple_greatest_common_divisor/g_c_d.rls" 

986 
"simple_greatest_common_divisor/g_c_d.siv" 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

987 
document_files 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

988 
"complex_types.ads" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

989 
"complex_types_app.adb" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

990 
"complex_types_app.ads" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

991 
"Gcd.adb" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

992 
"Gcd.ads" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

993 
"intro.tex" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

994 
"loop_invariant.adb" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

995 
"loop_invariant.ads" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

996 
"root.bib" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

997 
"root.tex" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

998 
"Simple_Gcd.adb" 
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

999 
"Simple_Gcd.ads" 
48481  1000 

65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

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

1002 
options [document = false] 
48481  1003 
theories MutabelleExtra 
1004 

65569
3cb6f3281ef1
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65563
diff
changeset

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

1006 
options [document = false] 
48588  1007 
theories 
48690  1008 
Quickcheck_Examples 
1009 
Quickcheck_Lattice_Examples 

1010 
Completeness 

1011 
Quickcheck_Interfaces 

63731
9f906a2eb0e7
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
63643
diff
changeset

1012 
Quickcheck_Nesting_Example 
57584
155b7e3b729e
proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
wenzelm
parents:
57544
diff
changeset

1013 
theories [condition = ISABELLE_GHC] 
57544
8840fa17e17c
reactivate session Quickcheck_Examples
Andreas Lochbihler
parents:
57543
diff
changeset

1014 
Hotel_Example 
48598  1015 
Quickcheck_Narrowing_Examples 
48588  1016 

65569
3cb6f3281ef1
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65563
diff
changeset

1017 
session "HOLQuotient_Examples" (timing) in Quotient_Examples = "HOLAlgebra" + 
48481  1018 
description {* 
1019 
Author: Cezary Kaliszyk and Christian Urban 

1020 
*} 

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

1021 
options [document = false] 
48481  1022 
theories 
1023 
DList 

63920
003622e08379
resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
kuncar
parents:
63888
diff
changeset

1024 
Quotient_FSet 
48481  1025 
Quotient_Int 
1026 
Quotient_Message 

1027 
Lift_FSet 

1028 
Lift_Set 

1029 
Lift_Fun 

1030 
Quotient_Rat 

1031 
Lift_DList 

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

1032 
Int_Pow 
60237  1033 
Lifting_Code_Dt_Test 
48481  1034 

65569
3cb6f3281ef1
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65563
diff
changeset

1035 
session "HOLPredicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOLLibrary" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

1036 
options [document = false] 
62354  1037 
theories 
48481  1038 
Examples 
1039 
Predicate_Compile_Tests 

61140
78ece168f5b5
reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents:
60921
diff
changeset

1040 
Predicate_Compile_Quickcheck_Examples 
48481  1041 
Specialisation_Examples 
48690  1042 
IMP_1 
1043 
IMP_2 

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

1044 
(* FIXME since 21Jul2011 
61140
78ece168f5b5
reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents:
60921
diff
changeset

1045 
Hotel_Example_Small_Generator *) 
48690  1046 
IMP_3 
61140
78ece168f5b5
reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents:
60921
diff
changeset

1047 
IMP_4 
62242
a4e6ea45f416
guard sessions that no longer work with SML/NJ  memory problems;
wenzelm
parents:
62168
diff
changeset

1048 
theories [condition = ISABELLE_SWIPL] 
48690  1049 
Code_Prolog_Examples 
1050 
Context_Free_Grammar_Example 

1051 
Hotel_Example_Prolog 

1052 
Lambda_Example 

1053 
List_Examples 

62242
a4e6ea45f416
guard sessions that no longer work with SML/NJ  memory problems;
wenzelm
parents:
62168
diff
changeset

1054 
theories [condition = ISABELLE_SWIPL, quick_and_dirty] 
48690  1055 
Reg_Exp_Example 
48481  1056 

64551  1057 
session "HOLTypes_To_Sets" in Types_To_Sets = HOL + 
1058 
description {* 

1059 
Experimental extension of HigherOrder Logic to allow translation of types to sets. 

1060 
*} 

1061 
options [document = false] 

1062 
theories 

1063 
Types_To_Sets 

1064 
"Examples/Prerequisites" 

1065 
"Examples/Finite" 

1066 
"Examples/T2_Spaces" 

1067 

63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset

1068 
session HOLCF (main timing) in HOLCF = HOL + 
48338  1069 
description {* 
1070 
Author: Franz Regensburger 

1071 
Author: Brian Huffman 

1072 

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

1074 
*} 

65543  1075 
sessions 
1076 
"HOLLibrary" 

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

1077 
theories [document = false] 
48338  1078 
"~~/src/HOL/Library/Nat_Bijection" 
1079 
"~~/src/HOL/Library/Countable" 

48481  1080 
theories 
65382  1081 
HOLCF (global) 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

1082 
document_files "root.tex" 
48481  1083 

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

1084 
session "HOLCFTutorial" in "HOLCF/Tutorial" = HOLCF + 
48481  1085 
theories 
1086 
Domain_ex 

1087 
Fixrec_ex 

1088 
New_Domain 

56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

1089 
document_files "root.tex" 
48481  1090 

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

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

1092 
options [document = false] 
65570  1093 
theories 
1094 
HOLCF_Library 

1095 
HOL_Cpo 

48481  1096 

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

1097 
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

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

1099 
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

1100 

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

1101 
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

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

1103 
options [document = false] 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

1104 
sessions 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

1105 
"HOLIMP" 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

1106 
theories 
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

1107 
HoareEx 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

1108 
document_files "root.tex" 
48338  1109 

65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

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

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

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

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

1114 
options [document = false] 
48481  1115 
theories 
1116 
Dnat 

1117 
Dagstuhl 

1118 
Focus_ex 

1119 
Fix2 

1120 
Hoare 

1121 
Concurrency_Monad 

1122 
Loop 

1123 
Powerdomain_ex 

1124 
Domain_Proofs 

1125 
Letrec 

1126 
Pattern_Match 

1127 

65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

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

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

1130 
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

1131 

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

1132 
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

1133 

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

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

1135 
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

1136 

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

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

1138 
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

1139 

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

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

1141 
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

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

1143 
options [document = false] 
48481  1144 
theories 
1145 
Fstreams 

1146 
FOCUS 

1147 
Buffer_adm 

1148 

63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset

1149 
session IOA (timing) in "HOLCF/IOA" = HOLCF + 
48481  1150 
description {* 
1151 
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

1152 
Copyright 1997 TU München 
48481  1153 

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

1154 
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

1155 

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

1156 
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

1157 
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

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

1160 
options [document = false] 
65538  1161 
theories Abstraction 
48481  1162 

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

1163 
session "IOAABP" in "HOLCF/IOA/ABP" = IOA + 
48481  1164 
description {* 
1165 
Author: Olaf Mueller 

1166 

1167 
The Alternating Bit Protocol performed in I/OAutomata. 

1168 
*} 

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

1169 
options [document = false] 
59503  1170 
theories 
1171 
Correctness 

1172 
Spec 

48481  1173 

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

1174 
session "IOANTP" in "HOLCF/IOA/NTP" = IOA + 
48481  1175 
description {* 
1176 
Author: Tobias Nipkow & Konrad Slind 

1177 

1178 
A network transmission protocol, performed in the 

1179 
I/O automata formalization by Olaf Mueller. 

1180 
*} 

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

1181 
options [document = false] 
48481  1182 
theories Correctness 
1183 

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

1184 
session "IOAStorage" in "HOLCF/IOA/Storage" = IOA + 
48481  1185 
description {* 
1186 
Author: Olaf Mueller 

1187 

1188 
Memory storage case study. 

1189 
*} 

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

1190 
options [document = false] 
48481  1191 
theories Correctness 
1192 

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

1193 
session "IOAex" in "HOLCF/IOA/ex" = IOA + 
48481  1194 
description {* 
1195 
Author: Olaf Mueller 

1196 
*} 

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

1197 
options [document = false] 
48481  1198 
theories 
1199 
TrivEx 

1200 
TrivEx2 