author  wenzelm 
Fri, 21 Apr 2017 20:07:51 +0200  
changeset 65543  8369b33fda0a 
parent 65538  a39ef48fbee0 
child 65544  c09c11386ca5 
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 
GCD 
09c00a304c00
include imports that morally belong to Main and are used in HOLProofs applications;
wenzelm
parents:
65509
diff
changeset

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

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

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

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

31 
"Tools/Quickcheck/PNF_Narrowing_Engine.hs" 
48338  32 

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

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

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

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

36 
*} 
48481  37 
theories 
38 
Library 

64588  39 
(*conflicting type class instantiations and dependent applications*) 
40 
Finite_Lattice 

41 
List_lexord 

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

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

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

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

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

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

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

49 
Code_Char 
55447  50 
Code_Prolog 
48481  51 
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

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

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

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

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

56 
RBT_Set 
64588  57 
(*prototypic tools*) 
58 
Predicate_Compile_Quickcheck 

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

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

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

61 
Old_Recdef 
58110
019c0211ed1f
took out legacy material from 'HOL/Library/Library.thy'
blanchet
parents:
58039
diff
changeset

62 
Old_SMT 
64588  63 
Refute 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

64 
document_files "root.bib" "root.tex" 
48481  65 

65375  66 
session "HOLAnalysis" (main timing) in Analysis = HOL + 
65543  67 
sessions 
68 
"HOLLibrary" 

69 
"HOLComputational_Algebra" 

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

71 
Analysis 
65375  72 
document_files 
73 
"root.tex" 

74 

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

76 
theories 

77 
Approximations 

78 
Circle_Area 

79 

65485  80 
session "HOLComputational_Algebra" in "Computational_Algebra" = HOL + 
65543  81 
sessions 
82 
"HOLLibrary" 

65417  83 
theories 
84 
Computational_Algebra 

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

86 
Field_as_Ring 

87 
Polynomial_Factorial 

88 

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

89 
session "HOLHahn_Banach" in Hahn_Banach = HOL + 
48481  90 
description {* 
91 
Author: Gertrud Bauer, TU Munich 

92 

93 
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

94 

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

95 
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

96 
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

97 
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

98 
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

99 

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

100 
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

101 
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

102 

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

103 
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

104 
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

105 
continous linearform on the whole vectorspace. 
48481  106 
*} 
65543  107 
sessions 
108 
"HOLLibrary" 

109 
theories 

110 
Hahn_Banach 

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

111 
document_files "root.bib" "root.tex" 
48481  112 

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

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

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

115 
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

116 

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

117 
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

118 
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

119 

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

120 
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

121 
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

122 

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

123 
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

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

125 
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

126 

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

127 
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

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

129 
*} 
65543  130 
sessions 
131 
"HOLLibrary" 

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

132 
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

133 
"~~/src/HOL/Library/Old_Datatype" 
48481  134 
theories [quick_and_dirty] 
135 
Common_Patterns 

136 
theories 

61935  137 
Nested_Datatype 
48481  138 
QuoDataType 
139 
QuoNestedDataType 

140 
Term 

141 
SList 

142 
ABexp 

143 
Tree 

144 
Ordinals 

145 
Sigma_Algebra 

146 
Comb 

147 
PropLog 

148 
Com 

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

149 
document_files "root.tex" 
48481  150 

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

151 
session "HOLIMP" (timing) in IMP = HOL + 
59446  152 
options [document_variants = document] 
48481  153 
theories [document = false] 
154 
"~~/src/HOL/Library/While_Combinator" 

155 
"~~/src/HOL/Library/Char_ord" 

156 
"~~/src/HOL/Library/List_lexord" 

51625  157 
"~~/src/HOL/Library/Quotient_List" 
158 
"~~/src/HOL/Library/Extended" 

48481  159 
theories 
160 
BExp 

161 
ASM 

50050  162 
Finite_Reachable 
52394  163 
Denotational 
52400  164 
Compiler2 
48481  165 
Poly_Types 
166 
Sec_Typing 

167 
Sec_TypingT 

52726  168 
Def_Init_Big 
169 
Def_Init_Small 

170 
Fold 

48481  171 
Live 
172 
Live_True 

173 
Hoare_Examples 

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

174 
Hoare_Sound_Complete 
52269  175 
VCG 
52282  176 
Hoare_Total 
63538
d7b5e2a222c2
added new vcg based on existentially quantified whilerule
nipkow
parents:
63537
diff
changeset

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

179 
Collecting_Examples 
48481  180 
Abs_Int_Tests 
181 
Abs_Int1_parity 

182 
Abs_Int1_const 

183 
Abs_Int3 

184 
Procs_Dyn_Vars_Dyn 

185 
Procs_Stat_Vars_Dyn 

186 
Procs_Stat_Vars_Stat 

187 
C_like 

188 
OO 

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

189 
document_files "root.bib" "root.tex" 
48481  190 

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

191 
session "HOLIMPP" in IMPP = HOL + 
48481  192 
description {* 
193 
Author: David von Oheimb 

194 
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

195 

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

196 
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

197 

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

198 
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

199 
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

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

202 
options [document = false] 
48481  203 
theories EvenOdd 
204 

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

205 
session "HOLData_Structures" (timing) in Data_Structures = HOL + 
61203  206 
options [document_variants = document] 
207 
theories [document = false] 

65538  208 
Less_False 
62706  209 
"~~/src/HOL/Library/Multiset" 
64323  210 
"~~/src/HOL/Number_Theory/Fib" 
61203  211 
theories 
63829  212 
Balance 
61203  213 
Tree_Map 
61232  214 
AVL_Map 
61224  215 
RBT_Map 
61469
cd82b1023932
added 23 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
61368
diff
changeset

216 
Tree23_Map 
61514  217 
Tree234_Map 
61789  218 
Brother12_Map 
62130  219 
AA_Map 
61525  220 
Splay_Map 
62706  221 
Leftist_Heap 
61224  222 
document_files "root.tex" "root.bib" 
61203  223 

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

224 
session "HOLImport" in Import = HOL + 
48481  225 
theories HOL_Light_Maps 
226 
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 

227 

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

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

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

230 
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

231 
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

232 
*} 
65543  233 
sessions 
234 
"HOLLibrary" 

235 
"HOLAlgebra" 

236 
"HOLComputational_Algebra" 

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

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

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

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

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

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

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

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

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

245 
"root.tex" 
48481  246 

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

247 
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

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

249 
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

250 
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

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

253 
document_files "root.bib" "root.tex" 
48481  254 

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

255 
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

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

257 
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

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

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

261 
document_files "root.bib" "root.tex" 
48481  262 

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

263 
session "HOLCodegenerator_Test" in Codegenerator_Test = "HOLLibrary" + 
62354  264 
options [document = false, browser_info = false] 
65543  265 
sessions 
266 
"HOLComputational_Algebra" 

267 
"HOLNumber_Theory" 

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

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

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

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

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

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

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

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

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

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

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

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

283 
Code_Test_SMLNJ 
48481  284 

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

285 
session "HOLMetis_Examples" (timing) in Metis_Examples = HOL + 
48481  286 
description {* 
287 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

288 
Author: Jasmin Blanchette, TU Muenchen 

289 

290 
Testing Metis and Sledgehammer. 

291 
*} 

58423  292 
options [document = false] 
48481  293 
theories 
294 
Abstraction 

295 
Big_O 

296 
Binary_Tree 

297 
Clausification 

298 
Message 

299 
Proxies 

300 
Tarski 

301 
Trans_Closure 

302 
Sets 

303 

55072  304 
session "HOLNitpick_Examples" in Nitpick_Examples = HOL + 
48481  305 
description {* 
306 
Author: Jasmin Blanchette, TU Muenchen 

307 
Copyright 2009 

308 
*} 

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

309 
options [document = false] 
48481  310 
theories [quick_and_dirty] Nitpick_Examples 
311 

64389  312 
session "HOLNunchaku" in Nunchaku = HOL + 
313 
description {* 

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

315 
Copyright 2015, 2016 

316 

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

318 
*} 

319 
options [document = false] 

320 
theories Nunchaku 

321 

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

322 
session "HOLAlgebra" (main timing) in Algebra = HOL + 
48481  323 
description {* 
324 
Author: Clemens Ballarin, started 24 September 1999 

325 

326 
The Isabelle Algebraic Library. 

327 
*} 

65543  328 
sessions 
329 
"HOLLibrary" 

330 
"HOLComputational_Algebra" 

48481  331 
theories [document = false] 
332 
(* Preliminaries from set and number theory *) 

333 
"~~/src/HOL/Library/FuncSet" 

65417  334 
"~~/src/HOL/Computational_Algebra/Primes" 
48481  335 
"~~/src/HOL/Library/Permutation" 
336 
theories 

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

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

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

339 

48481  340 
(* Groups *) 
341 
FiniteProduct (* Product operator for commutative groups *) 

342 
Sylow (* Sylow's theorem *) 

343 
Bij (* Automorphism Groups *) 

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

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

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

346 
Multiplicative_Group 
48481  347 

348 
(* Rings *) 

349 
Divisibility (* Rings *) 

350 
IntRing (* Ideals and residue classes *) 

351 
UnivPoly (* Polynomials *) 

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

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

353 
document_files "root.bib" "root.tex" 
48481  354 

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

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

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

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

358 
*} 
48481  359 
theories 
360 
Auth_Shared 

361 
Auth_Public 

362 
"Smartcard/Auth_Smartcard" 

363 
"Guard/Auth_Guard_Shared" 

364 
"Guard/Auth_Guard_Public" 

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

365 
document_files "root.tex" 
48481  366 

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

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

370 
Copyright 1998 University of Cambridge 

371 

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

372 
Verifying security protocols using Chandy and Misra's UNITY formalism. 
48481  373 
*} 
374 
theories 

375 
(*Basic metatheory*) 

65538  376 
UNITY_Main 
48481  377 

378 
(*Simple examples: no composition*) 

379 
"Simple/Deadlock" 

380 
"Simple/Common" 

381 
"Simple/Network" 

382 
"Simple/Token" 

383 
"Simple/Channel" 

384 
"Simple/Lift" 

385 
"Simple/Mutex" 

386 
"Simple/Reach" 

387 
"Simple/Reachability" 

388 

389 
(*Verifying security protocols using UNITY*) 

390 
"Simple/NSP_Bad" 

391 

392 
(*Example of composition*) 

393 
"Comp/Handshake" 

394 

395 
(*Universal properties examples*) 

396 
"Comp/Counter" 

397 
"Comp/Counterc" 

398 
"Comp/Priority" 

399 

400 
"Comp/TimerArray" 

401 
"Comp/Progress" 

402 

403 
"Comp/Alloc" 

404 
"Comp/AllocImpl" 

405 
"Comp/Client" 

406 

407 
(*obsolete*) 

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

409 
document_files "root.tex" 
48481  410 

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

411 
session "HOLUnix" in Unix = HOL + 
48481  412 
options [print_mode = "no_brackets,no_type_brackets"] 
413 
theories Unix 

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

414 
document_files "root.bib" "root.tex" 
48481  415 

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

416 
session "HOLZF" in ZF = HOL + 
48481  417 
theories MainZF Games 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

418 
document_files "root.tex" 
48481  419 

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

420 
session "HOLImperative_HOL" in Imperative_HOL = HOL + 
59446  421 
options [print_mode = "iff,no_brackets"] 
65543  422 
sessions 
423 
"HOLLibrary" 

48481  424 
theories [document = false] 
425 
"~~/src/HOL/Library/Countable" 

426 
"~~/src/HOL/Library/Monad_Syntax" 

427 
"~~/src/HOL/Library/LaTeXsugar" 

428 
theories Imperative_HOL_ex 

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

429 
document_files "root.bib" "root.tex" 
48481  430 

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

431 
session "HOLDecision_Procs" (timing) in Decision_Procs = HOL + 
51544  432 
description {* 
433 
Various decision procedures, typically involving reflection. 

434 
*} 

62354  435 
options [document = false] 
65543  436 
sessions 
437 
"HOLLibrary" 

438 
"HOLAlgebra" 

439 
theories 

440 
Decision_Procs 

48481  441 

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

442 
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

443 
options [document = false] 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
52400
diff
changeset

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

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

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

447 
XML_Data 
48481  448 

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

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

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

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

452 
*} 
62354  453 
options [parallel_proofs = 0, quick_and_dirty = false] 
65543  454 
sessions 
455 
"HOLLibrary" 

456 
"HOLComputational_Algebra" 

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

458 
"~~/src/HOL/Library/Code_Target_Numeral" 
48481  459 
"~~/src/HOL/Library/Monad_Syntax" 
65417  460 
"~~/src/HOL/Computational_Algebra/Primes" 
48481  461 
"~~/src/HOL/Library/State_Monad" 
462 
theories 

463 
Greatest_Common_Divisor 

464 
Warshall 

465 
Higman_Extraction 

466 
Pigeonhole 

467 
Euclid 

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

468 
document_files "root.bib" "root.tex" 
48481  469 

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

470 
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

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

472 
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

473 

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

474 
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

475 
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

476 

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

477 
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

478 
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

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

481 
parallel_proofs = 0, quick_and_dirty = false] 
65543  482 
sessions 
483 
"HOLLibrary" 

48481  484 
theories 
485 
Eta 

486 
StrongNorm 

487 
Standardization 

488 
WeakNorm 

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

489 
document_files "root.bib" "root.tex" 
48481  490 

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

491 
session "HOLProlog" in Prolog = HOL + 
48481  492 
description {* 
493 
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

494 

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

495 
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

496 

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

497 
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

498 
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

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

501 
options [document = false] 
48481  502 
theories Test Type 
503 

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

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

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

506 
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

507 
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

508 
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

509 
*} 
65543  510 
sessions 
511 
"HOLLibrary" 

59446  512 
theories [document = false] 
513 
"~~/src/HOL/Library/While_Combinator" 

514 
theories 

515 
MicroJava 

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

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

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

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

519 
"root.tex" 
48481  520 

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

521 
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

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

523 
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

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

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

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

528 
session "HOLBali" (timing) in Bali = HOL + 
48481  529 
theories 
530 
AxExample 

531 
AxSound 

532 
AxCompl 

533 
Trans 

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

535 
document_files "root.tex" 
48481  536 

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

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

539 
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

540 
Copyright 19941996 TU Muenchen 
48481  541 

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

542 
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

543 
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

544 
proofs of two communication protocols which formerly have been here. 
48481  545 

546 
@inproceedings{NipkowSlindIOA, 

547 
author={Tobias Nipkow and Konrad Slind}, 

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

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

550 
publisher=Springer, 

551 
series=LNCS, 

552 
note={To appear}} 

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

554 

555 
and 

556 

557 
@inproceedings{MuellerNipkow, 

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

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

560 
booktitle={Proc.\ TACAS Workshop}, 

561 
organization={Aarhus University, BRICS report}, 

562 
year=1995} 

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

564 
*} 

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

565 
options [document = false] 
48481  566 
theories Solve 
567 

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

568 
session "HOLLattice" in Lattice = HOL + 
48481  569 
description {* 
570 
Author: Markus Wenzel, TU Muenchen 

571 

572 
Basic theory of lattices and orders. 

573 
*} 

574 
theories CompleteLattice 

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

575 
document_files "root.tex" 
48481  576 

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

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

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

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

580 
*} 
65543  581 
sessions 
582 
"HOLLibrary" 

583 
"HOLNumber_Theory" 

48481  584 
theories [document = false] 
585 
"~~/src/HOL/Library/State_Monad" 

50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
49985
diff
changeset

586 
Code_Binary_Nat_examples 
48481  587 
"~~/src/HOL/Library/FuncSet" 
588 
Eval_Examples 

589 
Normalization_by_Evaluation 

590 
Hebrew 

591 
Chinese 

592 
Serbian 

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

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

595 
Cartouche_Examples 
64959  596 
Computations 
48481  597 
theories 
59090  598 
Commands 
57507  599 
Adhoc_Overloading_Examples 
48481  600 
Iff_Oracle 
601 
Coercion_Examples 

64920  602 
Peano_Axioms 
48481  603 
Guess 
62999  604 
Functions 
48481  605 
Induction_Schema 
606 
LocaleTest2 

607 
Records 

608 
While_Combinator_Example 

609 
MonoidGroup 

610 
BinEx 

611 
Hex_Bin_Examples 

612 
Antiquote 

613 
Multiquote 

614 
PER 

615 
NatSum 

616 
ThreeDivides 

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

617 
Cubic_Quartic 
59739  618 
Pythagoras 
48481  619 
Intuitionistic 
620 
CTL 

621 
Arith_Examples 

622 
Tree23 

58644  623 
Bubblesort 
48481  624 
MergeSort 
625 
Lagrange 

626 
Groebner_Examples 

627 
Unification 

628 
Primrec 

629 
Tarski 

630 
Classical 

631 
Set_Theory 

632 
Termination 

633 
Coherent 

634 
PresburgerEx 

51093  635 
Reflection_Examples 
48481  636 
Sqrt 
637 
Sqrt_Script 

61368  638 
Transfer_Debug 
48481  639 
Transfer_Ex 
640 
Transfer_Int_Nat 

56922  641 
Transitive_Closure_Table_Ex 
48481  642 
HarmonicSeries 
643 
Refute_Examples 

644 
Execute_Choice 

645 
Gauge_Integration 

646 
Dedekind_Real 

647 
Quicksort 

648 
Birthday_Paradox 

649 
List_to_Set_Comprehension_Examples 

650 
Seq 

651 
Simproc_Tests 

652 
Executable_Relation 

55663  653 
Set_Comprehension_Pointfree_Examples 
48481  654 
Parallel_Example 
50138  655 
IArray_Examples 
53430  656 
Simps_Case_Conv_Examples 
53935  657 
ML 
59739  658 
Rewrite_Examples 
56815  659 
SAT_Examples 
58630  660 
SOS 
58418  661 
SOS_Cert 
60603
09ecbd791d4a
add examples from Freek's top 100 theorems (thms 30, 73, 77)
bulwahn
parents:
60470
diff
changeset

662 
Ballot 
09ecbd791d4a
add examples from Freek's top 100 theorems (thms 30, 73, 77)
bulwahn
parents:
60470
diff
changeset

663 
Erdoes_Szekeres 
09ecbd791d4a
add examples from Freek's top 100 theorems (thms 30, 73, 77)
bulwahn
parents:
60470
diff
changeset

664 
Sum_of_Powers 
62285  665 
Sudoku 
63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
63091
diff
changeset

666 
Code_Timing 
63375
59803048b0e8
basic facts about almost everywhere fix bijections
haftmann
parents:
63283
diff
changeset

667 
Perm_Fragments 
63960
3daf02070be5
new proof method "argo" for a combination of quantifierfree propositional logic with equality and linear real arithmetic
boehmes
parents:
63920
diff
changeset

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

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

670 
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

671 
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

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

673 
document_files "root.bib" "root.tex" 
48481  674 

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

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

676 
description {* 
61935  677 
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

678 
*} 
61939  679 
options [quick_and_dirty] 
65543  680 
sessions 
681 
"HOLLibrary" 

682 
"HOLComputational_Algebra" 

48481  683 
theories [document = false] 
684 
"~~/src/HOL/Library/Lattice_Syntax" 

65417  685 
"../Computational_Algebra/Primes" 
48481  686 
theories 
61939  687 
Knaster_Tarski 
688 
Peirce 

689 
Drinker 

48481  690 
Cantor 
61939  691 
Structured_Statements 
692 
Basic_Logic 

48481  693 
Expr_Compiler 
694 
Fibonacci 

695 
Group 

696 
Group_Context 

697 
Group_Notepad 

698 
Hoare_Ex 

699 
Mutilated_Checkerboard 

700 
Puzzle 

701 
Summation 

61935  702 
First_Order_Logic 
703 
Higher_Order_Logic 

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

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

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

706 
"root.tex" 
48481  707 

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

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

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

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

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

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

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

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

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

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

717 

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

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

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

720 
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

721 
*} 
65543  722 
sessions 
723 
"HOLLibrary" 

724 
theories [document = false] 

725 
"~~/src/HOL/Library/Nat_Bijection" 

726 
theories 

727 
SET_Protocol 

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

728 
document_files "root.tex" 
48481  729 

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

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

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

732 
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

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

735 
document_files "root.tex" 
48481  736 

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

737 
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

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

739 
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

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

741 
options [document = false] 
48481  742 
theories TLA 
743 

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

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

745 
options [document = false] 
48481  746 
theories Inc 
747 

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

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

749 
options [document = false] 
48481  750 
theories DBuffer 
751 

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

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

753 
options [document = false] 
48481  754 
theories MemoryImplementation 
755 

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

756 
session "HOLTPTP" in TPTP = HOL + 
48481  757 
description {* 
758 
Author: Jasmin Blanchette, TU Muenchen 

759 
Author: Nik Sultana, University of Cambridge 

760 
Copyright 2011 

761 

762 
TPTPrelated extensions. 

763 
*} 

62354  764 
options [document = false] 
48481  765 
theories 
766 
ATP_Theory_Export 

767 
MaSh_Eval 

768 
TPTP_Interpret 

769 
THF_Arith 

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

770 
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

771 
theories 
48481  772 
ATP_Problem_Import 
773 

65382  774 
session "HOLProbability" (main timing) in "Probability" = "HOLAnalysis" + 
65543  775 
sessions 
776 
"HOLLibrary" 

48481  777 
theories [document = false] 
778 
"~~/src/HOL/Library/Countable" 

779 
"~~/src/HOL/Library/Permutation" 

56994  780 
"~~/src/HOL/Library/Order_Continuity" 
781 
"~~/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

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

785 
document_files "root.tex" 
48481  786 

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

787 
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

788 
theories 
65538  789 
Dining_Cryptographers 
790 
Koepf_Duermuth_Countermeasure 

791 
Measure_Not_CCC 

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

792 

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

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

794 
options [document = false] 
48481  795 
theories Nominal 
796 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

821 
VC_Condition 
48481  822 

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

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

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

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

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

827 
options [document = false] 
59747  828 
theories 
829 
Cardinals 

830 
Bounded_Set 

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

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

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

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

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

835 

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

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

837 
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

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

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

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

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

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

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

845 
TreeFsetI 
49872  846 
"Derivation_Trees/Gram_Lang" 
847 
"Derivation_Trees/Parallel" 

50517  848 
Koenig 
60921  849 
Lift_BNF 
61745  850 
Milner_Tofte 
54961  851 
Stream_Processor 
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset

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

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

856 

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

857 
session "HOLCorec_Examples" (timing) in Corec_Examples = HOL + 
62694  858 
description {* 
859 
Corecursion Examples. 

860 
*} 

861 
options [document = false] 

862 
theories 

863 
LFilter 

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

867 
"Tests/Iterate_GPV" 
62696  868 
theories [quick_and_dirty] 
869 
"Tests/GPV_Bare_Bones" 

870 
"Tests/Merge_D" 

871 
"Tests/Merge_Poly" 

872 
"Tests/Misc_Mono" 

873 
"Tests/Misc_Poly" 

874 
"Tests/Small_Concrete" 

62725  875 
"Tests/Stream_Friends" 
62696  876 
"Tests/TLList_Friends" 
63190  877 
"Tests/Type_Class" 
62694  878 

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

879 
session "HOLWord" (main timing) in Word = HOL + 
65382  880 
theories 
65462
db1827610513
less global theories  conflict with AFP entries;
wenzelm
parents:
65456
diff
changeset

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

882 
document_files "root.bib" "root.tex" 
48481  883 

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

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

885 
options [document = false] 
48481  886 
theories WordExamples 
887 

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

888 
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

889 
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

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

891 
document_files "root.tex" 
48481  892 

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

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

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

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

896 
*} 
62479  897 
theories 
898 
Nonstandard_Analysis 

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

899 
document_files "root.tex" 
48481  900 

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

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

902 
options [document = false] 
65543  903 
sessions 
904 
"HOLComputational_Algebra" 

905 
theories 

906 
NSPrimes 

48481  907 

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

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

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

911 

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

912 
session "HOLMirabelleex" in "Mirabelle/ex" = "HOLMirabelle" + 
62354  913 
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

914 
theories Ex 
48481  915 

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

916 
session "HOLWordSMT_Examples" (timing) in SMT_Examples = "HOLWord" + 
62354  917 
options [document = false, quick_and_dirty] 
48481  918 
theories 
52722  919 
Boogie 
48481  920 
SMT_Examples 
921 
SMT_Word_Examples 

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

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

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

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

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

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

928 
"VCC_Max.certs" 
48481  929 

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

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

931 
options [document = false] 
65382  932 
theories 
933 
SPARK (global) 

48481  934 

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

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

936 
options [document = false, spark_prv = false] 
48481  937 
theories 
938 
"Gcd/Greatest_Common_Divisor" 

939 

940 
"Liseq/Longest_Increasing_Subsequence" 

941 

942 
"RIPEMD160/F" 

943 
"RIPEMD160/Hash" 

944 
"RIPEMD160/K_L" 

945 
"RIPEMD160/K_R" 

946 
"RIPEMD160/R_L" 

947 
"RIPEMD160/Round" 

948 
"RIPEMD160/R_R" 

949 
"RIPEMD160/S_L" 

950 
"RIPEMD160/S_R" 

951 

952 
"Sqrt/Sqrt" 

953 
files 

954 
"Gcd/greatest_common_divisor/g_c_d.fdl" 

955 
"Gcd/greatest_common_divisor/g_c_d.rls" 

956 
"Gcd/greatest_common_divisor/g_c_d.siv" 

957 
"Liseq/liseq/liseq_length.fdl" 

958 
"Liseq/liseq/liseq_length.rls" 

959 
"Liseq/liseq/liseq_length.siv" 

960 
"RIPEMD160/rmd/f.fdl" 

961 
"RIPEMD160/rmd/f.rls" 

962 
"RIPEMD160/rmd/f.siv" 

963 
"RIPEMD160/rmd/hash.fdl" 

964 
"RIPEMD160/rmd/hash.rls" 

965 
"RIPEMD160/rmd/hash.siv" 

966 
"RIPEMD160/rmd/k_l.fdl" 

967 
"RIPEMD160/rmd/k_l.rls" 

968 
"RIPEMD160/rmd/k_l.siv" 

969 
"RIPEMD160/rmd/k_r.fdl" 

970 
"RIPEMD160/rmd/k_r.rls" 

971 
"RIPEMD160/rmd/k_r.siv" 

972 
"RIPEMD160/rmd/r_l.fdl" 

973 
"RIPEMD160/rmd/r_l.rls" 

974 
"RIPEMD160/rmd/r_l.siv" 

975 
"RIPEMD160/rmd/round.fdl" 

976 
"RIPEMD160/rmd/round.rls" 

977 
"RIPEMD160/rmd/round.siv" 

978 
"RIPEMD160/rmd/r_r.fdl" 

979 
"RIPEMD160/rmd/r_r.rls" 

980 
"RIPEMD160/rmd/r_r.siv" 

981 
"RIPEMD160/rmd/s_l.fdl" 

982 
"RIPEMD160/rmd/s_l.rls" 

983 
"RIPEMD160/rmd/s_l.siv" 

984 
"RIPEMD160/rmd/s_r.fdl" 

985 
"RIPEMD160/rmd/s_r.rls" 

986 
"RIPEMD160/rmd/s_r.siv" 

987 

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

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

989 
options [show_question_marks = false, spark_prv = false] 
48481  990 
theories 
991 
Example_Verification 

992 
VC_Principles 

993 
Reference 

994 
Complex_Types 

995 
files 

996 
"complex_types_app/initialize.fdl" 

997 
"complex_types_app/initialize.rls" 

998 
"complex_types_app/initialize.siv" 

999 
"loop_invariant/proc1.fdl" 

1000 
"loop_invariant/proc1.rls" 

1001 
"loop_invariant/proc1.siv" 

1002 
"loop_invariant/proc2.fdl" 

1003 
"loop_invariant/proc2.rls" 

1004 
"loop_invariant/proc2.siv" 

1005 
"simple_greatest_common_divisor/g_c_d.fdl" 

1006 
"simple_greatest_common_divisor/g_c_d.rls" 

1007 
"simple_greatest_common_divisor/g_c_d.siv" 

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

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

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

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

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

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

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

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

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

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

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

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

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

1020 
"Simple_Gcd.ads" 
48481  1021 

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

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

1023 
options [document = false] 
48481  1024 
theories MutabelleExtra 
1025 

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

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

1027 
options [document = false] 
48588  1028 
theories 
48690  1029 
Quickcheck_Examples 
1030 
Quickcheck_Lattice_Examples 

1031 
Completeness 

1032 
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

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

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

1035 
Hotel_Example 
48598  1036 
Quickcheck_Narrowing_Examples 
48588  1037 

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

1038 
session "HOLQuotient_Examples" (timing) in Quotient_Examples = HOL + 
48481  1039 
description {* 
1040 
Author: Cezary Kaliszyk and Christian Urban 

1041 
*} 

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

1042 
options [document = false] 
65543  1043 
sessions 
1044 
"HOLLibrary" 

48481  1045 
theories 
1046 
DList 

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

1047 
Quotient_FSet 
48481  1048 
Quotient_Int 
1049 
Quotient_Message 

1050 
Lift_FSet 

1051 
Lift_Set 

1052 
Lift_Fun 

1053 
Quotient_Rat 

1054 
Lift_DList 

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

1055 
Int_Pow 
60237  1056 
Lifting_Code_Dt_Test 
48481  1057 

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

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

1059 
options [document = false] 
62354  1060 
theories 
48481  1061 
Examples 
1062 
Predicate_Compile_Tests 

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

1063 
Predicate_Compile_Quickcheck_Examples 
48481  1064 
Specialisation_Examples 
48690  1065 
IMP_1 
1066 
IMP_2 

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

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

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

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

1071 
theories [condition = ISABELLE_SWIPL] 
48690  1072 
Code_Prolog_Examples 
1073 
Context_Free_Grammar_Example 

1074 
Hotel_Example_Prolog 

1075 
Lambda_Example 

1076 
List_Examples 

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

1077 
theories [condition = ISABELLE_SWIPL, quick_and_dirty] 
48690  1078 
Reg_Exp_Example 
48481  1079 

64551  1080 
session "HOLTypes_To_Sets" in Types_To_Sets = HOL + 
1081 
description {* 

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

1083 
*} 

1084 
options [document = false] 

1085 
theories 

1086 
Types_To_Sets 

1087 
"Examples/Prerequisites" 

1088 
"Examples/Finite" 

1089 
"Examples/T2_Spaces" 

1090 

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

1091 
session HOLCF (main timing) in HOLCF = HOL + 
48338  1092 
description {* 
1093 
Author: Franz Regensburger 

1094 
Author: Brian Huffman 

1095 

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

1097 
*} 

65543  1098 
sessions 
1099 
"HOLLibrary" 

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

1100 
theories [document = false] 
48338  1101 
"~~/src/HOL/Library/Nat_Bijection" 
1102 
"~~/src/HOL/Library/Countable" 

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

1105 
document_files "root.tex" 
48481  1106 

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

1107 
session "HOLCFTutorial" in "HOLCF/Tutorial" = HOLCF + 
48481  1108 
theories 
1109 
Domain_ex 

1110 
Fixrec_ex 

1111 
New_Domain 

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

1112 
document_files "root.tex" 
48481  1113 

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

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

1115 
options [document = false] 
48481  1116 
theories HOLCF_Library 
1117 

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

1118 
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

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

1120 
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

1121 

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

1122 
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

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

1124 
options [document = false] 
48481  1125 
theories HoareEx 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

1126 
document_files "root.tex" 
48338  1127 

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

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

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

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

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

1132 
options [document = false] 
48481  1133 
theories 
1134 
Dnat 

1135 
Dagstuhl 

1136 
Focus_ex 

1137 
Fix2 

1138 
Hoare 

1139 
Concurrency_Monad 

1140 
Loop 

1141 
Powerdomain_ex 

1142 
Domain_Proofs 

1143 
Letrec 

1144 
Pattern_Match 

1145 

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

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

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

1148 
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

1149 

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

1150 
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

1151 

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

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

1153 
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

1154 

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

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

1156 
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

1157 

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

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

1159 
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

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

1161 
options [document = false] 
48481  1162 
theories 
1163 
Fstreams 

1164 
FOCUS 

1165 
Buffer_adm 

1166 

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

1167 
session IOA (timing) in "HOLCF/IOA" = HOLCF + 
48481  1168 
description {* 
1169 
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

1170 
Copyright 1997 TU München 
48481  1171 

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

1172 
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

1173 

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

1174 
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

1175 
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

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

1178 
options [document = false] 
65538  1179 
theories Abstraction 
48481  1180 

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

1181 
session "IOAABP" in "HOLCF/IOA/ABP" = IOA + 
48481  1182 
description {* 
1183 
Author: Olaf Mueller 

1184 

1185 
The Alternating Bit Protocol performed in I/OAutomata. 

1186 
*} 

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

1187 
options [document = false] 
59503  1188 
theories 
1189 
Correctness 

1190 
Spec 

48481  1191 

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

1192 
session "IOANTP" in "HOLCF/IOA/NTP" = IOA + 
48481  1193 
description {* 
1194 
Author: Tobias Nipkow & Konrad Slind 

1195 

1196 
A network transmission protocol, performed in the 

1197 
I/O automata formalization by Olaf Mueller. 

1198 
*} 

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

1199 
options [document = false] 
48481  1200 
theories Correctness 
1201 

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

1202 
session "IOAStorage" in "HOLCF/IOA/Storage" = IOA + 
48481  1203 
description {* 
1204 
Author: Olaf Mueller 

1205 

1206 
Memory storage case study. 

1207 
*} 

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

1208 
options [document = false] 
48481  1209 
theories Correctness 
1210 

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

1211 
session "IOAex" in "HOLCF/IOA/ex" = IOA + 
48481  1212 
description {* 
1213 
Author: Olaf Mueller 

1214 
*} 

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

1215 
options [document = false] 
48481  1216 
theories 
1217 
TrivEx 

1218 
TrivEx2 