author  Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de> 
Fri, 16 Oct 2020 19:34:37 +0200  
changeset 72486  e4d707eb7d1b 
parent 72478  b452242dce36 
child 72515  c7038c397ae3 
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 + 
69319  4 
description " 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

5 
Classical Higherorder Logic. 
69319  6 
" 
70678
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents:
70675
diff
changeset

7 
options [strict_facts] 
70853  8 
sessions Tools 
70796
2739631ac368
discontinued pointless dump_checkpoint and share_common_data  superseded by base logic image in Isabelle/MMT;
wenzelm
parents:
70781
diff
changeset

9 
theories 
65374  10 
Main (global) 
11 
Complex_Main (global) 

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

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

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

14 
"root.tex" 
48338  15 

71925
bf085daea304
clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
71924
diff
changeset

16 
session "HOLExamples" in Examples = HOL + 
bf085daea304
clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
71924
diff
changeset

17 
description " 
bf085daea304
clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
71924
diff
changeset

18 
Notable Examples in Isabelle/HOL. 
bf085daea304
clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
71924
diff
changeset

19 
" 
bf085daea304
clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
71924
diff
changeset

20 
sessions 
bf085daea304
clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
71924
diff
changeset

21 
"HOLLibrary" 
bf085daea304
clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
71924
diff
changeset

22 
theories 
72029  23 
Adhoc_Overloading_Examples 
71930  24 
Ackermann 
72029  25 
Cantor 
26 
Coherent 

27 
Commands 

71925
bf085daea304
clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
71924
diff
changeset

28 
Drinker 
72029  29 
Groebner_Examples 
30 
Iff_Oracle 

31 
Induction_Schema 

32 
Knaster_Tarski 

33 
"ML" 

34 
Peirce 

35 
Records 

71925
bf085daea304
clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
71924
diff
changeset

36 
Seq 
bf085daea304
clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
71924
diff
changeset

37 
document_files 
bf085daea304
clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
71924
diff
changeset

38 
"root.bib" 
bf085daea304
clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
71924
diff
changeset

39 
"root.tex" 
bf085daea304
clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
71924
diff
changeset

40 

bf085daea304
clarified sessions: "Notable Examples in Isabelle/HOL";
wenzelm
parents:
71924
diff
changeset

41 

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

44 
HOLMain with explicit proof terms. 
69319  45 
" 
70398  46 
options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500] 
65543  47 
sessions 
48 
"HOLLibrary" 

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

49 
theories 
67319
07176d5b81d5
moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
blanchet
parents:
67278
diff
changeset

50 
"HOLLibrary.Realizers" 
48338  51 

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

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

54 
Classical Higherorder Logic  batteries included. 
69319  55 
" 
48481  56 
theories 
57 
Library 

64588  58 
(*conflicting type class instantiations and dependent applications*) 
59 
Finite_Lattice 

68312  60 
List_Lexorder 
71766
1249b998e377
New theory Library/List_Lenlexorder.thy, a type class instantiation for wellordering lists
paulson <lp15@cam.ac.uk>
parents:
71518
diff
changeset

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

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

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

64 
Product_Order 
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65678
diff
changeset

65 
Subseq_Order 
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
67319
diff
changeset

66 
(*conflicting syntax*) 
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
67319
diff
changeset

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

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

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

70 
Code_Binary_Nat 
55447  71 
Code_Prolog 
48481  72 
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

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

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

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

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

77 
RBT_Set 
66015
70643edecb7a
specific output setup is not supposed to intrude regular import theory
haftmann
parents:
65956
diff
changeset

78 
(*printing modifications*) 
70643edecb7a
specific output setup is not supposed to intrude regular import theory
haftmann
parents:
65956
diff
changeset

79 
OptionalSugar 
64588  80 
(*prototypic tools*) 
81 
Predicate_Compile_Quickcheck 

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

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

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

84 
Old_Recdef 
67319
07176d5b81d5
moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
blanchet
parents:
67278
diff
changeset

85 
Realizers 
64588  86 
Refute 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

87 
document_files "root.bib" "root.tex" 
48481  88 

66932
149025fecca0
reduced heap hierarchy, for potentially improved performance;
wenzelm
parents:
66842
diff
changeset

89 
session "HOLAnalysis" (main timing) in Analysis = HOL + 
68617  90 
options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", 
67152
8021ea06aad8
just one session for bulky HOLAnalysis documents;
wenzelm
parents:
67122
diff
changeset

91 
document_variants = "document:manual=proof,ML,unimportant"] 
66932
149025fecca0
reduced heap hierarchy, for potentially improved performance;
wenzelm
parents:
66842
diff
changeset

92 
sessions 
67152
8021ea06aad8
just one session for bulky HOLAnalysis documents;
wenzelm
parents:
67122
diff
changeset

93 
"HOLLibrary" 
66932
149025fecca0
reduced heap hierarchy, for potentially improved performance;
wenzelm
parents:
66842
diff
changeset

94 
"HOLComputational_Algebra" 
70781
a37e2ea96c6d
just one dump_checkpoint Main  potentially more robust;
wenzelm
parents:
70678
diff
changeset

95 
theories 
65462
db1827610513
less global theories  conflict with AFP entries;
wenzelm
parents:
65456
diff
changeset

96 
Analysis 
65375  97 
document_files 
98 
"root.tex" 

69518  99 
"root.bib" 
65375  100 

71189
954ee5acaae0
Split off new HOLComplex_Analysis session from HOLAnalysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset

101 
session "HOLComplex_Analysis" (main timing) in Complex_Analysis = "HOLAnalysis" + 
954ee5acaae0
Split off new HOLComplex_Analysis session from HOLAnalysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset

102 
options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", 
954ee5acaae0
Split off new HOLComplex_Analysis session from HOLAnalysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset

103 
document_variants = "document:manual=proof,ML,unimportant"] 
954ee5acaae0
Split off new HOLComplex_Analysis session from HOLAnalysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset

104 
theories 
954ee5acaae0
Split off new HOLComplex_Analysis session from HOLAnalysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset

105 
Complex_Analysis 
954ee5acaae0
Split off new HOLComplex_Analysis session from HOLAnalysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset

106 
document_files 
954ee5acaae0
Split off new HOLComplex_Analysis session from HOLAnalysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset

107 
"root.tex" 
954ee5acaae0
Split off new HOLComplex_Analysis session from HOLAnalysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset

108 
"root.bib" 
954ee5acaae0
Split off new HOLComplex_Analysis session from HOLAnalysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset

109 

65375  110 
session "HOLAnalysisex" in "Analysis/ex" = "HOLAnalysis" + 
111 
theories 

112 
Approximations 

70956
860198428664
added examples for "metric" method, by Maximilian Schäffeler
immler
parents:
70853
diff
changeset

113 
Metric_Arith_Examples 
65375  114 

70151  115 
session "HOLHomology" (timing) in Homology = "HOLAnalysis" + 
70089
eca8611201e9
new Homology target, depending on HOLAlgebra and HOLAnalysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset

116 
options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", 
eca8611201e9
new Homology target, depending on HOLAlgebra and HOLAnalysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset

117 
document_variants = "document:manual=proof,ML,unimportant"] 
eca8611201e9
new Homology target, depending on HOLAlgebra and HOLAnalysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset

118 
sessions 
eca8611201e9
new Homology target, depending on HOLAlgebra and HOLAnalysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset

119 
"HOLAlgebra" 
eca8611201e9
new Homology target, depending on HOLAlgebra and HOLAnalysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset

120 
theories 
eca8611201e9
new Homology target, depending on HOLAlgebra and HOLAnalysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset

121 
Homology 
eca8611201e9
new Homology target, depending on HOLAlgebra and HOLAnalysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset

122 
document_files 
eca8611201e9
new Homology target, depending on HOLAlgebra and HOLAnalysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset

123 
"root.tex" 
eca8611201e9
new Homology target, depending on HOLAlgebra and HOLAnalysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset

124 

67100  125 
session "HOLComputational_Algebra" (main timing) in "Computational_Algebra" = "HOLLibrary" + 
65417  126 
theories 
127 
Computational_Algebra 

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

129 
Field_as_Ring 

130 

68630  131 
session "HOLReal_Asymp" in Real_Asymp = HOL + 
132 
sessions 

133 
"HOLDecision_Procs" 

134 
theories 

135 
Real_Asymp 

136 
Real_Asymp_Approx 

68677  137 
Real_Asymp_Examples 
138 

139 
session "HOLReal_AsympManual" in "Real_Asymp/Manual" = "HOLReal_Asymp" + 

140 
theories 

141 
Real_Asymp_Doc 

142 
document_files (in "~~/src/Doc") 

143 
"iman.sty" 

144 
"extra.sty" 

145 
"isar.sty" 

146 
document_files 

147 
"root.tex" 

148 
"style.sty" 

68630  149 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

150 
session "HOLHahn_Banach" in Hahn_Banach = HOL + 
69319  151 
description " 
48481  152 
Author: Gertrud Bauer, TU Munich 
153 

154 
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

155 

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

156 
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

157 
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

158 
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

159 
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

160 

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

161 
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

162 
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

163 

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

164 
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

165 
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

166 
continous linearform on the whole vectorspace. 
69319  167 
" 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

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

169 
"HOLAnalysis" 
65543  170 
theories 
171 
Hahn_Banach 

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

172 
document_files "root.bib" "root.tex" 
48481  173 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

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

176 
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

177 

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

178 
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

179 
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

180 

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

181 
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

182 
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

183 

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

184 
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

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

186 
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

187 

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

188 
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

189 
mutually recursive relations. 
69319  190 
" 
71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

191 
sessions 
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

192 
"HOLLibrary" 
48481  193 
theories [quick_and_dirty] 
194 
Common_Patterns 

195 
theories 

61935  196 
Nested_Datatype 
48481  197 
QuoDataType 
198 
QuoNestedDataType 

199 
Term 

200 
SList 

201 
ABexp 

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

202 
Infinitely_Branching_Tree 
48481  203 
Ordinals 
204 
Sigma_Algebra 

205 
Comb 

206 
PropLog 

207 
Com 

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

208 
document_files "root.tex" 
48481  209 

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

210 
session "HOLIMP" (timing) in IMP = "HOLLibrary" + 
59446  211 
options [document_variants = document] 
48481  212 
theories 
213 
BExp 

214 
ASM 

50050  215 
Finite_Reachable 
52394  216 
Denotational 
52400  217 
Compiler2 
48481  218 
Poly_Types 
219 
Sec_Typing 

220 
Sec_TypingT 

52726  221 
Def_Init_Big 
222 
Def_Init_Small 

223 
Fold 

48481  224 
Live 
225 
Live_True 

226 
Hoare_Examples 

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

227 
Hoare_Sound_Complete 
52269  228 
VCG 
52282  229 
Hoare_Total 
63538
d7b5e2a222c2
added new vcg based on existentially quantified whilerule
nipkow
parents:
63537
diff
changeset

230 
VCG_Total_EX 
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
66992
diff
changeset

231 
VCG_Total_EX2 
48481  232 
Collecting1 
48765
fb1ed5230abc
special code with lists no longer necessary, use sets
nipkow
parents:
48738
diff
changeset

233 
Collecting_Examples 
48481  234 
Abs_Int_Tests 
235 
Abs_Int1_parity 

236 
Abs_Int1_const 

237 
Abs_Int3 

238 
Procs_Dyn_Vars_Dyn 

239 
Procs_Stat_Vars_Dyn 

240 
Procs_Stat_Vars_Stat 

241 
C_like 

242 
OO 

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

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

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

245 
session "HOLIMPP" in IMPP = HOL + 
69272  246 
description \<open> 
48481  247 
Author: David von Oheimb 
248 
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

249 

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

250 
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

251 

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

252 
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

253 
procedures. For documentation see "Hoare Logic for Mutual Recursion and 
68649  254 
Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). 
69319  255 
\<close> 
48481  256 
theories EvenOdd 
257 

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

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

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

261 
"HOLNumber_Theory" 
61203  262 
theories [document = false] 
65538  263 
Less_False 
61203  264 
theories 
66543  265 
Sorting 
63829  266 
Balance 
61203  267 
Tree_Map 
71414  268 
Interval_Tree 
61232  269 
AVL_Map 
71814  270 
AVL_Bal_Set 
71844  271 
AVL_Bal2_Set 
71801  272 
Height_Balanced_Tree 
71352  273 
RBT_Set2 
61224  274 
RBT_Map 
61469
cd82b1023932
added 23 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
61368
diff
changeset

275 
Tree23_Map 
72099  276 
Tree23_of_List 
61514  277 
Tree234_Map 
61789  278 
Brother12_Map 
62130  279 
AA_Map 
68261  280 
Set2_Join_RBT 
69145  281 
Array_Braun 
70250  282 
Trie_Fun 
283 
Trie_Map 

284 
Tries_Binary 

72389  285 
Queue_2Lists 
62706  286 
Leftist_Heap 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66270
diff
changeset

287 
Binomial_Heap 
61224  288 
document_files "root.tex" "root.bib" 
61203  289 

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

290 
session "HOLImport" in Import = HOL + 
48481  291 
theories HOL_Light_Maps 
292 
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 

293 

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

296 
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

297 
Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity. 
69319  298 
" 
65543  299 
sessions 
300 
"HOLAlgebra" 

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

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

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

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

304 
"root.tex" 
48481  305 

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

306 
session "HOLHoare" in Hoare = HOL + 
69319  307 
description " 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

308 
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

309 
automatically from pre/post conditions and loop invariants). 
69319  310 
" 
48481  311 
theories Hoare 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

312 
document_files "root.bib" "root.tex" 
48481  313 

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

314 
session "HOLHoare_Parallel" (timing) in Hoare_Parallel = HOL + 
69319  315 
description " 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

316 
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

317 
(verification conditions are generated automatically). 
69319  318 
" 
48481  319 
theories Hoare_Parallel 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

320 
document_files "root.bib" "root.tex" 
48481  321 

72312  322 
session "HOLCodegenerator_Test" in Codegenerator_Test = "HOLLibrary" + 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

323 
sessions 
72312  324 
"HOLNumber_Theory" 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

325 
"HOLData_Structures" 
72056  326 
"HOLExamples" 
327 
"HOLWord" 

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

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

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

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

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

332 
Generate_Efficient_Datastructures 
68155  333 
Code_Lazy_Test 
64582
3d20ded18f14
unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
wenzelm
parents:
64569
diff
changeset

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

335 
Code_Test_Scala 
66842  336 
theories [condition = ISABELLE_GHC] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

337 
Code_Test_GHC 
66842  338 
theories [condition = ISABELLE_MLTON] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

339 
Code_Test_MLton 
69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69716
diff
changeset

340 
theories [condition = ISABELLE_OCAMLFIND] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

341 
Code_Test_OCaml 
66842  342 
theories [condition = ISABELLE_SMLNJ] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

343 
Code_Test_SMLNJ 
48481  344 

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

345 
session "HOLMetis_Examples" (timing) in Metis_Examples = "HOLLibrary" + 
69319  346 
description " 
48481  347 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
348 
Author: Jasmin Blanchette, TU Muenchen 

349 

350 
Testing Metis and Sledgehammer. 

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

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

353 
"HOLDecision_Procs" 
48481  354 
theories 
355 
Abstraction 

356 
Big_O 

357 
Binary_Tree 

358 
Clausification 

359 
Message 

360 
Proxies 

361 
Tarski 

362 
Trans_Closure 

363 
Sets 

364 

72189
7a213affdc10
clarified session: no parent image for minor theory imports;
wenzelm
parents:
72102
diff
changeset

365 
session "HOLNitpick_Examples" in Nitpick_Examples = HOL + 
69319  366 
description " 
48481  367 
Author: Jasmin Blanchette, TU Muenchen 
368 
Copyright 2009 

69319  369 
" 
72189
7a213affdc10
clarified session: no parent image for minor theory imports;
wenzelm
parents:
72102
diff
changeset

370 
sessions "HOLLibrary" 
48481  371 
theories [quick_and_dirty] Nitpick_Examples 
372 

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

373 
session "HOLAlgebra" (main timing) in Algebra = "HOLComputational_Algebra" + 
69319  374 
description " 
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68522
diff
changeset

375 
Author: Clemens Ballarin, started 24 September 1999, and many others 
48481  376 

377 
The Isabelle Algebraic Library. 

69319  378 
" 
70660
373d95cf1b98
proper sessionqualifier imports (amending "fixes" from adaa0a6ea4fe);
wenzelm
parents:
70646
diff
changeset

379 
sessions 
373d95cf1b98
proper sessionqualifier imports (amending "fixes" from adaa0a6ea4fe);
wenzelm
parents:
70646
diff
changeset

380 
"HOLCardinals" 
48481  381 
theories 
65099
30d0b2f1df76
KnasterTarski fixed point theorem and Galois Connections.
ballarin
parents:
65050
diff
changeset

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

383 
Galois_Connection (* KnasterTarski theorem and Galois connections *) 
48481  384 
(* Groups *) 
385 
FiniteProduct (* Product operator for commutative groups *) 

386 
Sylow (* Sylow's theorem *) 

387 
Bij (* Automorphism Groups *) 

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

388 
Multiplicative_Group 
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset

389 
Zassenhaus (* The Zassenhaus lemma *) 
48481  390 
(* Rings *) 
391 
Divisibility (* Rings *) 

392 
IntRing (* Ideals and residue classes *) 

393 
UnivPoly (* Polynomials *) 

68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68522
diff
changeset

394 
(* Main theory *) 
70078  395 
Algebra 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

396 
document_files "root.bib" "root.tex" 
48481  397 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

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

400 
A new approach to verifying authentication protocols. 
69319  401 
" 
71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

402 
sessions "HOLLibrary" 
70675  403 
directories "Smartcard" "Guard" 
48481  404 
theories 
405 
Auth_Shared 

406 
Auth_Public 

407 
"Smartcard/Auth_Smartcard" 

408 
"Guard/Auth_Guard_Shared" 

409 
"Guard/Auth_Guard_Public" 

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

410 
document_files "root.tex" 
48481  411 

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

412 
session "HOLUNITY" (timing) in UNITY = "HOLAuth" + 
69319  413 
description " 
48481  414 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
415 
Copyright 1998 University of Cambridge 

416 

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

417 
Verifying security protocols using Chandy and Misra's UNITY formalism. 
69319  418 
" 
70675  419 
directories "Simple" "Comp" 
48481  420 
theories 
421 
(*Basic metatheory*) 

65538  422 
UNITY_Main 
48481  423 

424 
(*Simple examples: no composition*) 

425 
"Simple/Deadlock" 

426 
"Simple/Common" 

427 
"Simple/Network" 

428 
"Simple/Token" 

429 
"Simple/Channel" 

430 
"Simple/Lift" 

431 
"Simple/Mutex" 

432 
"Simple/Reach" 

433 
"Simple/Reachability" 

434 

435 
(*Verifying security protocols using UNITY*) 

436 
"Simple/NSP_Bad" 

437 

438 
(*Example of composition*) 

439 
"Comp/Handshake" 

440 

441 
(*Universal properties examples*) 

442 
"Comp/Counter" 

443 
"Comp/Counterc" 

444 
"Comp/Priority" 

445 

446 
"Comp/TimerArray" 

447 
"Comp/Progress" 

448 

449 
"Comp/Alloc" 

450 
"Comp/AllocImpl" 

451 
"Comp/Client" 

452 

453 
(*obsolete*) 

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

455 
document_files "root.tex" 
48481  456 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

457 
session "HOLUnix" in Unix = HOL + 
48481  458 
options [print_mode = "no_brackets,no_type_brackets"] 
71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

459 
sessions "HOLLibrary" 
48481  460 
theories Unix 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

461 
document_files "root.bib" "root.tex" 
48481  462 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

463 
session "HOLZF" in ZF = HOL + 
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

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

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

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

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

468 
document_files "root.tex" 
48481  469 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

470 
session "HOLImperative_HOL" (timing) in Imperative_HOL = HOL + 
70678
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents:
70675
diff
changeset

471 
options [print_mode = "iff,no_brackets"] 
71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

472 
sessions "HOLLibrary" 
70675  473 
directories "ex" 
48481  474 
theories Imperative_HOL_ex 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

475 
document_files "root.bib" "root.tex" 
48481  476 

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

477 
session "HOLDecision_Procs" (timing) in Decision_Procs = "HOLAlgebra" + 
69319  478 
description " 
51544  479 
Various decision procedures, typically involving reflection. 
69319  480 
" 
70675  481 
directories "ex" 
65543  482 
theories 
483 
Decision_Procs 

48481  484 

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

485 
session "HOLProofsex" in "Proofs/ex" = "HOLProofs" + 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

486 
sessions 
72049  487 
"HOLExamples" 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
52400
diff
changeset

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

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

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

491 
XML_Data 
48481  492 

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

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

495 
Examples for program extraction in HigherOrder Logic. 
69319  496 
" 
70398  497 
options [quick_and_dirty = false] 
65543  498 
sessions 
499 
"HOLComputational_Algebra" 

48481  500 
theories 
501 
Greatest_Common_Divisor 

502 
Warshall 

503 
Higman_Extraction 

504 
Pigeonhole 

505 
Euclid 

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

506 
document_files "root.bib" "root.tex" 
48481  507 

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

508 
session "HOLProofsLambda" (timing) in "Proofs/Lambda" = "HOLProofs" + 
69272  509 
description \<open> 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

510 
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

511 

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

512 
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

513 
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

514 

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

515 
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

516 
theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). 
69319  517 
\<close> 
70398  518 
options [print_mode = "no_brackets", quick_and_dirty = false] 
65543  519 
sessions 
520 
"HOLLibrary" 

48481  521 
theories 
522 
Eta 

523 
StrongNorm 

524 
Standardization 

525 
WeakNorm 

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

526 
document_files "root.bib" "root.tex" 
48481  527 

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

528 
session "HOLProlog" in Prolog = HOL + 
69319  529 
description " 
48481  530 
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

531 

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

532 
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

533 

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

534 
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

535 
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

536 
a little functional language and its type system. 
69319  537 
" 
48481  538 
theories Test Type 
539 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

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

542 
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

543 
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

544 
bytecode verifier, including proofs of typesafety. 
69319  545 
" 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

546 
sessions 
71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

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

548 
"HOLEisbach" 
70678
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents:
70675
diff
changeset

549 
directories "BV" "Comp" "DFA" "J" "JVM" 
59446  550 
theories 
551 
MicroJava 

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

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

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

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

555 
"root.tex" 
48481  556 

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

557 
session "HOLNanoJava" in NanoJava = HOL + 
69319  558 
description " 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

559 
Hoare Logic for a tiny fragment of Java. 
69319  560 
" 
48481  561 
theories Example 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

562 
document_files "root.bib" "root.tex" 
48481  563 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

564 
session "HOLBali" (timing) in Bali = HOL + 
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

565 
sessions 
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

566 
"HOLLibrary" 
48481  567 
theories 
568 
AxExample 

569 
AxSound 

570 
AxCompl 

571 
Trans 

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

573 
document_files "root.tex" 
48481  574 

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

575 
session "HOLIOA" in IOA = HOL + 
69272  576 
description \<open> 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

577 
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

578 
Copyright 19941996 TU Muenchen 
48481  579 

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

580 
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

581 
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

582 
proofs of two communication protocols which formerly have been here. 
48481  583 

584 
@inproceedings{NipkowSlindIOA, 

585 
author={Tobias Nipkow and Konrad Slind}, 

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

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

588 
publisher=Springer, 

589 
series=LNCS, 

590 
note={To appear}} 

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

592 

593 
and 

594 

595 
@inproceedings{MuellerNipkow, 

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

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

598 
booktitle={Proc.\ TACAS Workshop}, 

599 
organization={Aarhus University, BRICS report}, 

600 
year=1995} 

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

69319  602 
\<close> 
48481  603 
theories Solve 
604 

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

605 
session "HOLLattice" in Lattice = HOL + 
69319  606 
description " 
48481  607 
Author: Markus Wenzel, TU Muenchen 
608 

609 
Basic theory of lattices and orders. 

69319  610 
" 
48481  611 
theories CompleteLattice 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

612 
document_files "root.tex" 
48481  613 

66752  614 
session "HOLex" (timing) in ex = "HOLNumber_Theory" + 
69319  615 
description " 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

616 
Miscellaneous examples for HigherOrder Logic. 
69319  617 
" 
72102  618 
sessions 
619 
"HOLWord" 

65548  620 
theories 
48481  621 
Antiquote 
65549  622 
Argo_Examples 
623 
Arith_Examples 

624 
Ballot 

625 
BinEx 

626 
Birthday_Paradox 

67909
f55b07f4d1ee
proof of concept for algebraically founded bit lists
haftmann
parents:
67612
diff
changeset

627 
Bit_Lists 
65549  628 
Bubblesort 
629 
CTL 

630 
Cartouche_Examples 

65563  631 
Case_Product 
65549  632 
Chinese 
633 
Classical 

634 
Code_Binary_Nat_examples 

68639  635 
Code_Lazy_Demo 
65549  636 
Code_Timing 
637 
Coercion_Examples 

638 
Computations 

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

640 
Cubic_Quartic 
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
67319
diff
changeset

641 
Datatype_Record_Examples 
65549  642 
Dedekind_Real 
643 
Erdoes_Szekeres 

644 
Eval_Examples 

645 
Executable_Relation 

646 
Execute_Choice 

647 
Functions 

66797  648 
Function_Growth 
65549  649 
Gauge_Integration 
650 
Guess 

651 
HarmonicSeries 

652 
Hebrew 

653 
Hex_Bin_Examples 

654 
IArray_Examples 

48481  655 
Intuitionistic 
70525  656 
Join_Theory 
65549  657 
Lagrange 
658 
List_to_Set_Comprehension_Examples 

659 
LocaleTest2 

48481  660 
MergeSort 
65549  661 
MonoidGroup 
662 
Multiquote 

663 
NatSum 

664 
Normalization_by_Evaluation 

665 
PER 

666 
Parallel_Example 

667 
Peano_Axioms 

668 
Perm_Fragments 

669 
PresburgerEx 

48481  670 
Primrec 
65549  671 
Pythagoras 
672 
Quicksort 

67612  673 
Radix_Sort 
65549  674 
Reflection_Examples 
675 
Refute_Examples 

68035
6d7cc6723978
proof of concept for residue rings over int using type numerals
haftmann
parents:
68028
diff
changeset

676 
Residue_Ring 
65549  677 
Rewrite_Examples 
678 
SOS 

679 
SOS_Cert 

680 
Serbian 

681 
Set_Comprehension_Pointfree_Examples 

48481  682 
Set_Theory 
65549  683 
Simproc_Tests 
684 
Simps_Case_Conv_Examples 

70018
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
69926
diff
changeset

685 
Sketch_and_Explore 
69252  686 
Sorting_Algorithms_Examples 
48481  687 
Sqrt 
688 
Sqrt_Script 

65549  689 
Sudoku 
690 
Sum_of_Powers 

691 
Tarski 

692 
Termination 

693 
ThreeDivides 

61368  694 
Transfer_Debug 
48481  695 
Transfer_Int_Nat 
56922  696 
Transitive_Closure_Table_Ex 
65549  697 
Tree23 
69716  698 
Triangular_Numbers 
65549  699 
Unification 
700 
While_Combinator_Example 

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

701 
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

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

704 
Meson_Test 
48481  705 

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

706 
session "HOLIsar_Examples" in Isar_Examples = "HOLComputational_Algebra" + 
69319  707 
description " 
61935  708 
Miscellaneous Isabelle/Isar examples. 
69319  709 
" 
61939  710 
options [quick_and_dirty] 
48481  711 
theories 
61939  712 
Structured_Statements 
713 
Basic_Logic 

48481  714 
Expr_Compiler 
715 
Fibonacci 

716 
Group 

717 
Group_Context 

718 
Group_Notepad 

719 
Hoare_Ex 

720 
Mutilated_Checkerboard 

721 
Puzzle 

722 
Summation 

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

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

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

725 
"root.tex" 
48481  726 

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

727 
session "HOLEisbach" in Eisbach = HOL + 
69272  728 
description \<open> 
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset

729 
The Eisbach proof method language and "match" method. 
69319  730 
\<close> 
66444  731 
sessions 
732 
FOL 

70958
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
70956
diff
changeset

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

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

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

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

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

738 
Examples_FOL 
70958
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
70956
diff
changeset

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

740 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

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

743 
Verification of the SET Protocol. 
69319  744 
" 
71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

745 
sessions 
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

746 
"HOLLibrary" 
65543  747 
theories 
748 
SET_Protocol 

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

749 
document_files "root.tex" 
48481  750 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

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

753 
Twodimensional matrices and linear programming. 
69319  754 
" 
71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

755 
sessions "HOLLibrary" 
70675  756 
directories "Compute_Oracle" 
48481  757 
theories Cplex 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

758 
document_files "root.tex" 
48481  759 

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

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

762 
Lamport's Temporal Logic of Actions. 
69319  763 
" 
48481  764 
theories TLA 
765 

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

766 
session "HOLTLAInc" in "TLA/Inc" = "HOLTLA" + 
48481  767 
theories Inc 
768 

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

769 
session "HOLTLABuffer" in "TLA/Buffer" = "HOLTLA" + 
48481  770 
theories DBuffer 
771 

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

772 
session "HOLTLAMemory" in "TLA/Memory" = "HOLTLA" + 
48481  773 
theories MemoryImplementation 
774 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

775 
session "HOLTPTP" in TPTP = HOL + 
69319  776 
description " 
48481  777 
Author: Jasmin Blanchette, TU Muenchen 
778 
Author: Nik Sultana, University of Cambridge 

779 
Copyright 2011 

780 

781 
TPTPrelated extensions. 

69319  782 
" 
71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

783 
sessions 
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

784 
"HOLLibrary" 
48481  785 
theories 
786 
ATP_Theory_Export 

787 
MaSh_Eval 

788 
TPTP_Interpret 

789 
THF_Arith 

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

790 
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

791 
theories 
48481  792 
ATP_Problem_Import 
793 

65382  794 
session "HOLProbability" (main timing) in "Probability" = "HOLAnalysis" + 
70781
a37e2ea96c6d
just one dump_checkpoint Main  potentially more robust;
wenzelm
parents:
70678
diff
changeset

795 
theories 
66992
69673025292e
less global theories  avoid confusion about special cases;
wenzelm
parents:
66986
diff
changeset

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

797 
document_files "root.tex" 
48481  798 

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

799 
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

800 
theories 
65538  801 
Dining_Cryptographers 
802 
Koepf_Duermuth_Countermeasure 

803 
Measure_Not_CCC 

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

804 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

805 
session "HOLNominal" in Nominal = HOL + 
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

806 
sessions "HOLLibrary" 
70781
a37e2ea96c6d
just one dump_checkpoint Main  potentially more robust;
wenzelm
parents:
70678
diff
changeset

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

808 
Nominal 
48481  809 

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

810 
session "HOLNominalExamples" (timing) in "Nominal/Examples" = "HOLNominal" + 
58329
a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents:
58313
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

833 
VC_Condition 
48481  834 

70078  835 
session "HOLCardinals" (timing) in Cardinals = HOL + 
69319  836 
description " 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

837 
Ordinals and Cardinals, Full Theories. 
69319  838 
" 
59747  839 
theories 
840 
Cardinals 

841 
Bounded_Set 

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

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

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

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

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

846 

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

847 
session "HOLDatatype_Examples" (timing) in Datatype_Examples = "HOLLibrary" + 
69319  848 
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

849 
(Co)datatype Examples. 
69319  850 
" 
70675  851 
directories "Derivation_Trees" 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset

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

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

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

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

858 
"Derivation_Trees/Parallel_Composition" 
50517  859 
Koenig 
60921  860 
Lift_BNF 
61745  861 
Milner_Tofte 
54961  862 
Stream_Processor 
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
71352
diff
changeset

863 
Cyclic_List 
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
71352
diff
changeset

864 
Free_Idempotent_Monoid 
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
71352
diff
changeset

865 
LDL 
71263
35a92ce0b94e
an extensive example for lift_bnf across quotients
traytel
parents:
71189
diff
changeset

866 
TLList 
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset

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

868 
Misc_Datatype 
54193  869 
Misc_Primcorec 
53306  870 
Misc_Primrec 
71836
c095d3143047
New HOL simproc 'datatype_no_proper_subterm'
Manuel Eberl <eberlm@in.tum.de>
parents:
71832
diff
changeset

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

872 

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

873 
session "HOLCorec_Examples" (timing) in Corec_Examples = "HOLLibrary" + 
69319  874 
description " 
62694  875 
Corecursion Examples. 
69319  876 
" 
70675  877 
directories "Tests" 
62694  878 
theories 
879 
LFilter 

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

883 
"Tests/Iterate_GPV" 
62696  884 
theories [quick_and_dirty] 
885 
"Tests/GPV_Bare_Bones" 

886 
"Tests/Merge_D" 

887 
"Tests/Merge_Poly" 

888 
"Tests/Misc_Mono" 

889 
"Tests/Misc_Poly" 

890 
"Tests/Small_Concrete" 

62725  891 
"Tests/Stream_Friends" 
62696  892 
"Tests/TLList_Friends" 
63190  893 
"Tests/Type_Class" 
62694  894 

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

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

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

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

899 
Word 
70174  900 
More_Word 
70173  901 
Word_Examples 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

902 
document_files "root.bib" "root.tex" 
48481  903 

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

904 
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

905 
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

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

907 
document_files "root.tex" 
48481  908 

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

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

911 
Nonstandard analysis. 
69319  912 
" 
62479  913 
theories 
914 
Nonstandard_Analysis 

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

915 
document_files "root.tex" 
48481  916 

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

917 
session "HOLNonstandard_AnalysisExamples" (timing) in "Nonstandard_Analysis/Examples" = "HOLNonstandard_Analysis" + 
65543  918 
theories 
919 
NSPrimes 

48481  920 

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

921 
session "HOLMirabelle" in Mirabelle = HOL + 
48481  922 
theories Mirabelle_Test 
48589
fb446a780d50
separate session HOLMirabelleex  cannot run isolated shell scripts within build tool;
wenzelm
parents:
48588
diff
changeset

923 

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

924 
session "HOLMirabelleex" in "Mirabelle/ex" = "HOLMirabelle" + 
66946
3d8fd98c7c86
ROOT cleanup: empty 'document_files' means there is no document;
wenzelm
parents:
66932
diff
changeset

925 
options [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

926 
theories Ex 
48481  927 

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

928 
session "HOLWordSMT_Examples" (timing) in SMT_Examples = "HOLWord" + 
66946
3d8fd98c7c86
ROOT cleanup: empty 'document_files' means there is no document;
wenzelm
parents:
66932
diff
changeset

929 
options [quick_and_dirty] 
48481  930 
theories 
52722  931 
Boogie 
48481  932 
SMT_Examples 
933 
SMT_Word_Examples 

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

934 
SMT_Tests 
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
72389
diff
changeset

935 
SMT_Tests_Verit 
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
72389
diff
changeset

936 
SMT_Examples_Verit 
48481  937 

69093  938 
session "HOLSPARK" in "SPARK" = "HOLWord" + 
65382  939 
theories 
66992
69673025292e
less global theories  avoid confusion about special cases;
wenzelm
parents:
66986
diff
changeset

940 
SPARK 
48481  941 

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

942 
session "HOLSPARKExamples" in "SPARK/Examples" = "HOLSPARK" + 
70675  943 
directories "Gcd" "Liseq" "RIPEMD160" "Sqrt" 
48481  944 
theories 
945 
"Gcd/Greatest_Common_Divisor" 

946 
"Liseq/Longest_Increasing_Subsequence" 

947 
"RIPEMD160/F" 

948 
"RIPEMD160/Hash" 

949 
"RIPEMD160/K_L" 

950 
"RIPEMD160/K_R" 

951 
"RIPEMD160/R_L" 

952 
"RIPEMD160/Round" 

953 
"RIPEMD160/R_R" 

954 
"RIPEMD160/S_L" 

955 
"RIPEMD160/S_R" 

956 
"Sqrt/Sqrt" 

70026  957 
export_files (in ".") "*:**.prv" 
48481  958 

65576  959 
session "HOLSPARKManual" in "SPARK/Manual" = "HOLSPARK" + 
69099
d44cb8a3e5e0
HOLSPARK .prv files are no longer written to the filesystem;
wenzelm
parents:
69093
diff
changeset

960 
options [show_question_marks = false] 
66031  961 
sessions 
962 
"HOLSPARKExamples" 

48481  963 
theories 
964 
Example_Verification 

965 
VC_Principles 

966 
Reference 

967 
Complex_Types 

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

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

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

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

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

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

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

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

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

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

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

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

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

980 
"Simple_Gcd.ads" 
48481  981 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

982 
session "HOLMutabelle" in Mutabelle = HOL + 
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

983 
sessions "HOLLibrary" 
48481  984 
theories MutabelleExtra 
985 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

986 
session "HOLQuickcheck_Examples" (timing) in Quickcheck_Examples = HOL + 
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

987 
sessions "HOLLibrary" 
48588  988 
theories 
48690  989 
Quickcheck_Examples 
990 
Quickcheck_Lattice_Examples 

991 
Completeness 

992 
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

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

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

995 
Hotel_Example 
48598  996 
Quickcheck_Narrowing_Examples 
48588  997 

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

998 
session "HOLQuotient_Examples" (timing) in Quotient_Examples = "HOLAlgebra" + 
69319  999 
description " 
48481  1000 
Author: Cezary Kaliszyk and Christian Urban 
69319  1001 
" 
48481  1002 
theories 
1003 
DList 

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

1004 
Quotient_FSet 
48481  1005 
Quotient_Int 
1006 
Quotient_Message 

1007 
Lift_FSet 

1008 
Lift_Set 

1009 
Lift_Fun 

1010 
Quotient_Rat 

1011 
Lift_DList 

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

1012 
Int_Pow 
60237  1013 
Lifting_Code_Dt_Test 
48481  1014 

71832
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

1015 
session "HOLPredicate_Compile_Examples" (timing) in Predicate_Compile_Examples = HOL + 
f61b19358a8f
clarified session imports: avoid bulky HOLLibrary image;
wenzelm
parents:
71814
diff
changeset

1016 
sessions "HOLLibrary" 
62354  1017 
theories 
48481  1018 
Examples 
1019 
Predicate_Compile_Tests 

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

1020 
Predicate_Compile_Quickcheck_Examples 
48481  1021 
Specialisation_Examples 
48690  1022 
IMP_1 
1023 
IMP_2 

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

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

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

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

1028 
theories [condition = ISABELLE_SWIPL] 
48690  1029 
Code_Prolog_Examples 
1030 
Context_Free_Grammar_Example 

1031 
Hotel_Example_Prolog 

1032 
Lambda_Example 

1033 
List_Examples 

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

1034 
theories [condition = ISABELLE_SWIPL, quick_and_dirty] 
48690  1035 
Reg_Exp_Example 
48481  1036 

64551  1037 
session "HOLTypes_To_Sets" in Types_To_Sets = HOL + 
69319  1038 
description " 
64551  1039 
Experimental extension of HigherOrder Logic to allow translation of types to sets. 
69319  1040 
" 
70675  1041 
directories "Examples" 
64551  1042 
theories 
1043 
Types_To_Sets 

1044 
"Examples/Prerequisites" 

1045 
"Examples/Finite" 

1046 
"Examples/T2_Spaces" 

69689  1047 
"Examples/Unoverload_Def" 
68522
d9cbc1e8644d
example for Types_To_Sets: transfer from typebased linear algebra to subspaces
immler
parents:
68516
diff
changeset

1048 
"Examples/Linear_Algebra_On" 
64551  1049 

66982
67595389aa8a
build faster without heap images for minor imports;
wenzelm
parents:
66956
diff
changeset

1050 
session HOLCF (main timing) in HOLCF = HOL + 
69319  1051 
description " 
48338  1052 
Author: Franz Regensburger 
1053 
Author: Brian Huffman 

1054 

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

69319  1056 
" 
66982
67595389aa8a
build faster without heap images for minor imports;
wenzelm
parents:
66956
diff
changeset

1057 
sessions 
67595389aa8a
build faster without heap images for minor imports;
wenzelm
parents:
66956
diff
changeset

1058 
"HOLLibrary" 
48481  1059 
theories 
65382  1060 
HOLCF (global) 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

1061 
document_files "root.tex" 
48481  1062 

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

1063 
session "HOLCFTutorial" in "HOLCF/Tutorial" = HOLCF + 
48481  1064 
theories 
1065 
Domain_ex 

1066 
Fixrec_ex 

1067 
New_Domain 

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

1068 
document_files "root.tex" 
48481  1069 

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

1070 
session "HOLCFLibrary" in "HOLCF/Library" = HOLCF + 
65570  1071 
theories 
1072 
HOLCF_Library 

1073 
HOL_Cpo 

48481  1074 

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

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

1077 
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

1078 

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

1079 
This is the HOLCFbased denotational semantics of a simple WHILElanguage. 
69319  1080 
" 
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset

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

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

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

1084 
HoareEx 
66950  1085 
document_files 
1086 
"isaverbatimwrite.sty" 

1087 
"root.tex" 

1088 
"root.bib" 

48338  1089 

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

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

1092 
Miscellaneous examples for HOLCF. 
69319  1093 
" 
48481  1094 
theories 
1095 
Dnat 

1096 
Dagstuhl 

1097 
Focus_ex 

1098 
Fix2 

1099 
Hoare 

1100 
Concurrency_Monad 

1101 
Loop 

1102 
Powerdomain_ex 

1103 
Domain_Proofs 

1104 
Letrec 

1105 
Pattern_Match 

1106 

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

1107 
session "HOLCFFOCUS" in "HOLCF/FOCUS" = "HOLCFLibrary" + 
69272  1108 
description \<open> 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

1109 
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

1110 

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

1111 
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

1112 

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

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

1114 
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

1115 

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

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

1117 
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

1118 

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

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

1120 
Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321 
69319  1121 
\<close> 
48481  1122 
theories 
1123 
Fstreams 

1124 
FOCUS 

1125 
Buffer_adm 

1126 

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

1127 
session IOA (timing) in "HOLCF/IOA" = HOLCF + 
69319  1128 
description " 
48481  1129 
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

1130 
Copyright 1997 TU München 
48481  1131 

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

1132 
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

1133 

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

1134 
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

1135 
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

1136 
finite and infinite sequences. 
69319  1137 
" 
65538  1138 
theories Abstraction 
48481  1139 

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

1140 
session "IOAABP" in "HOLCF/IOA/ABP" = IOA + 
69319  1141 
description " 
48481  1142 
Author: Olaf Mueller 
1143 

1144 
The Alternating Bit Protocol performed in I/OAutomata. 

69319  1145 
" 
59503  1146 
theories 
1147 
Correctness 

1148 
Spec 

48481  1149 

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

1150 
session "IOANTP" in "HOLCF/IOA/NTP" = IOA + 
69319  1151 
description " 
48481  1152 
Author: Tobias Nipkow & Konrad Slind 
1153 

1154 
A network transmission protocol, performed in the 

1155 
I/O automata formalization by Olaf Mueller. 

69319  1156 
" 
48481  1157 
theories Correctness 
1158 

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

1159 
session "IOAStorage" in "HOLCF/IOA/Storage" = IOA + 
69319  1160 
description " 
48481  1161 
Author: Olaf Mueller 
1162 

1163 
Memory storage case study. 

69319  1164 
" 
48481  1165 
theories Correctness 
1166 

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

1167 
session "IOAex" in "HOLCF/IOA/ex" = IOA + 
69319  1168 
description " 
48481  1169 
Author: Olaf Mueller 
69319  1170 
" 
48481  1171 
theories 
1172 
TrivEx 

1173 
TrivEx2 