author  wenzelm 
Thu, 17 Aug 2017 14:40:42 +0200  
changeset 66445  407de0768126 
parent 66444  6d2d993fa76e 
child 66453  cc19f7ca2ed6 
permissions  rwrr 
51397
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
51263
diff
changeset

1 
chapter HOL 
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
51263
diff
changeset

2 

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

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

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

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

6 
*} 
65374  7 
theories 
8 
Main (global) 

9 
Complex_Main (global) 

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

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

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

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

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

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

15 
"root.tex" 
48338  16 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

34 
*} 
48481  35 
theories 
36 
Library 

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

39 
List_lexord 

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

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

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

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

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

44 
(*data refinements and dependent applications*) 
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset

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

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

47 
Code_Char 
55447  48 
Code_Prolog 
48481  49 
Code_Real_Approx_By_Float 
50023
28f3263d4d1b
refined stack of library theories implementing int and/or nat by target language numerals
haftmann
parents:
49985
diff
changeset

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

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

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

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

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

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

56 
OptionalSugar 
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 
64588  62 
Refute 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

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

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

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

67 
Analysis 
65375  68 
document_files 
69 
"root.tex" 

70 

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

72 
theories 

73 
Approximations 

74 
Circle_Area 

75 

65678  76 
session "HOLComputational_Algebra" (timing) in "Computational_Algebra" = "HOLLibrary" + 
65417  77 
theories 
78 
Computational_Algebra 

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

80 
Field_as_Ring 

81 
Polynomial_Factorial 

82 

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

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

86 

87 
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

88 

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

89 
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

90 
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

91 
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

92 
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

93 

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

94 
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

95 
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

96 

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

97 
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

98 
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

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

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

102 
"HOLAnalysis" 
65543  103 
theories 
104 
Hahn_Banach 

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

105 
document_files "root.bib" "root.tex" 
48481  106 

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

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

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

109 
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

110 

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

111 
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

112 
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

113 

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

114 
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

115 
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

116 

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

117 
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

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

119 
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

120 

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

121 
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

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

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

124 
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

125 
"~~/src/HOL/Library/Old_Datatype" 
48481  126 
theories [quick_and_dirty] 
127 
Common_Patterns 

128 
theories 

61935  129 
Nested_Datatype 
48481  130 
QuoDataType 
131 
QuoNestedDataType 

132 
Term 

133 
SList 

134 
ABexp 

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

135 
Infinitely_Branching_Tree 
48481  136 
Ordinals 
137 
Sigma_Algebra 

138 
Comb 

139 
PropLog 

140 
Com 

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

141 
document_files "root.tex" 
48481  142 

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

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

147 
"~~/src/HOL/Library/Char_ord" 

148 
"~~/src/HOL/Library/List_lexord" 

51625  149 
"~~/src/HOL/Library/Quotient_List" 
150 
"~~/src/HOL/Library/Extended" 

48481  151 
theories 
152 
BExp 

153 
ASM 

50050  154 
Finite_Reachable 
52394  155 
Denotational 
52400  156 
Compiler2 
48481  157 
Poly_Types 
158 
Sec_Typing 

159 
Sec_TypingT 

52726  160 
Def_Init_Big 
161 
Def_Init_Small 

162 
Fold 

48481  163 
Live 
164 
Live_True 

165 
Hoare_Examples 

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

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

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

171 
Collecting_Examples 
48481  172 
Abs_Int_Tests 
173 
Abs_Int1_parity 

174 
Abs_Int1_const 

175 
Abs_Int3 

176 
Procs_Dyn_Vars_Dyn 

177 
Procs_Stat_Vars_Dyn 

178 
Procs_Stat_Vars_Stat 

179 
C_like 

180 
OO 

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

181 
document_files "root.bib" "root.tex" 
48481  182 

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

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

186 
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

187 

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

188 
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

189 

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

190 
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

191 
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

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

194 
options [document = false] 
48481  195 
theories EvenOdd 
196 

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

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

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

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

210 
Tree23_Map 
61514  211 
Tree234_Map 
61789  212 
Brother12_Map 
62130  213 
AA_Map 
61525  214 
Splay_Map 
62706  215 
Leftist_Heap 
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66270
diff
changeset

216 
Binomial_Heap 
61224  217 
document_files "root.tex" "root.bib" 
61203  218 

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

219 
session "HOLImport" in Import = HOL + 
48481  220 
theories HOL_Light_Maps 
221 
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 

222 

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

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

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

225 
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

226 
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

227 
*} 
65543  228 
sessions 
229 
"HOLAlgebra" 

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

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

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

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

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

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

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

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

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

238 
"root.tex" 
48481  239 

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

240 
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

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

242 
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

243 
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

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

246 
document_files "root.bib" "root.tex" 
48481  247 

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

248 
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

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

250 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

276 
Code_Test_SMLNJ 
48481  277 

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

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

281 
Author: Jasmin Blanchette, TU Muenchen 

282 

283 
Testing Metis and Sledgehammer. 

284 
*} 

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

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

287 
"HOLDecision_Procs" 
48481  288 
theories 
289 
Abstraction 

290 
Big_O 

291 
Binary_Tree 

292 
Clausification 

293 
Message 

294 
Proxies 

295 
Tarski 

296 
Trans_Closure 

297 
Sets 

298 

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

299 
session "HOLNitpick_Examples" in Nitpick_Examples = "HOLLibrary" + 
48481  300 
description {* 
301 
Author: Jasmin Blanchette, TU Muenchen 

302 
Copyright 2009 

303 
*} 

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

304 
options [document = false] 
48481  305 
theories [quick_and_dirty] Nitpick_Examples 
306 

64389  307 
session "HOLNunchaku" in Nunchaku = HOL + 
308 
description {* 

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

310 
Copyright 2015, 2016 

311 

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

313 
*} 

314 
options [document = false] 

315 
theories Nunchaku 

316 

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

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

320 

321 
The Isabelle Algebraic Library. 

322 
*} 

323 
theories [document = false] 

324 
(* Preliminaries from set and number theory *) 

325 
"~~/src/HOL/Library/FuncSet" 

65417  326 
"~~/src/HOL/Computational_Algebra/Primes" 
48481  327 
"~~/src/HOL/Library/Permutation" 
328 
theories 

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

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

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

331 

48481  332 
(* Groups *) 
333 
FiniteProduct (* Product operator for commutative groups *) 

334 
Sylow (* Sylow's theorem *) 

335 
Bij (* Automorphism Groups *) 

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

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

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

338 
Multiplicative_Group 
48481  339 

340 
(* Rings *) 

341 
Divisibility (* Rings *) 

342 
IntRing (* Ideals and residue classes *) 

343 
UnivPoly (* Polynomials *) 

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

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

345 
document_files "root.bib" "root.tex" 
48481  346 

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

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

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

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

350 
*} 
48481  351 
theories 
352 
Auth_Shared 

353 
Auth_Public 

354 
"Smartcard/Auth_Smartcard" 

355 
"Guard/Auth_Guard_Shared" 

356 
"Guard/Auth_Guard_Public" 

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

357 
document_files "root.tex" 
48481  358 

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

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

362 
Copyright 1998 University of Cambridge 

363 

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

364 
Verifying security protocols using Chandy and Misra's UNITY formalism. 
48481  365 
*} 
366 
theories 

367 
(*Basic metatheory*) 

65538  368 
UNITY_Main 
48481  369 

370 
(*Simple examples: no composition*) 

371 
"Simple/Deadlock" 

372 
"Simple/Common" 

373 
"Simple/Network" 

374 
"Simple/Token" 

375 
"Simple/Channel" 

376 
"Simple/Lift" 

377 
"Simple/Mutex" 

378 
"Simple/Reach" 

379 
"Simple/Reachability" 

380 

381 
(*Verifying security protocols using UNITY*) 

382 
"Simple/NSP_Bad" 

383 

384 
(*Example of composition*) 

385 
"Comp/Handshake" 

386 

387 
(*Universal properties examples*) 

388 
"Comp/Counter" 

389 
"Comp/Counterc" 

390 
"Comp/Priority" 

391 

392 
"Comp/TimerArray" 

393 
"Comp/Progress" 

394 

395 
"Comp/Alloc" 

396 
"Comp/AllocImpl" 

397 
"Comp/Client" 

398 

399 
(*obsolete*) 

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

401 
document_files "root.tex" 
48481  402 

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

403 
session "HOLUnix" in Unix = "HOLLibrary" + 
48481  404 
options [print_mode = "no_brackets,no_type_brackets"] 
405 
theories Unix 

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

406 
document_files "root.bib" "root.tex" 
48481  407 

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

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

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

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

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

412 
document_files "root.tex" 
48481  413 

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

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

418 
"~~/src/HOL/Library/Monad_Syntax" 

419 
"~~/src/HOL/Library/LaTeXsugar" 

420 
theories Imperative_HOL_ex 

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

421 
document_files "root.bib" "root.tex" 
48481  422 

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

423 
session "HOLDecision_Procs" (timing) in Decision_Procs = "HOLAlgebra" + 
51544  424 
description {* 
425 
Various decision procedures, typically involving reflection. 

426 
*} 

62354  427 
options [document = false] 
65543  428 
theories 
429 
Decision_Procs 

48481  430 

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

431 
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

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

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

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

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

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

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

438 
XML_Data 
48481  439 

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

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

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

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

443 
*} 
62354  444 
options [parallel_proofs = 0, quick_and_dirty = false] 
65543  445 
sessions 
446 
"HOLLibrary" 

447 
"HOLComputational_Algebra" 

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

449 
"~~/src/HOL/Library/Code_Target_Numeral" 
48481  450 
"~~/src/HOL/Library/Monad_Syntax" 
65417  451 
"~~/src/HOL/Computational_Algebra/Primes" 
66270
403d84138c5c
State_Monad ~> Open_State_Syntax
Lars Hupel <lars.hupel@mytum.de>
parents:
66031
diff
changeset

452 
"~~/src/HOL/Library/Open_State_Syntax" 
48481  453 
theories 
454 
Greatest_Common_Divisor 

455 
Warshall 

456 
Higman_Extraction 

457 
Pigeonhole 

458 
Euclid 

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

459 
document_files "root.bib" "root.tex" 
48481  460 

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

461 
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

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

463 
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

464 

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

465 
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

466 
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

467 

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

468 
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

469 
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

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

472 
parallel_proofs = 0, quick_and_dirty = false] 
65543  473 
sessions 
474 
"HOLLibrary" 

48481  475 
theories 
476 
Eta 

477 
StrongNorm 

478 
Standardization 

479 
WeakNorm 

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

480 
document_files "root.bib" "root.tex" 
48481  481 

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

482 
session "HOLProlog" in Prolog = HOL + 
48481  483 
description {* 
484 
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

485 

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

486 
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

487 

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

488 
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

489 
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

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

492 
options [document = false] 
48481  493 
theories Test Type 
494 

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

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

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

497 
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

498 
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

499 
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

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

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

502 
"HOLEisbach" 
59446  503 
theories [document = false] 
504 
"~~/src/HOL/Library/While_Combinator" 

505 
theories 

506 
MicroJava 

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

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

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

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

510 
"root.tex" 
48481  511 

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

512 
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

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

514 
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

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

517 
document_files "root.bib" "root.tex" 
48481  518 

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

519 
session "HOLBali" (timing) in Bali = "HOLLibrary" + 
48481  520 
theories 
521 
AxExample 

522 
AxSound 

523 
AxCompl 

524 
Trans 

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

526 
document_files "root.tex" 
48481  527 

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

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

530 
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

531 
Copyright 19941996 TU Muenchen 
48481  532 

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

533 
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

534 
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

535 
proofs of two communication protocols which formerly have been here. 
48481  536 

537 
@inproceedings{NipkowSlindIOA, 

538 
author={Tobias Nipkow and Konrad Slind}, 

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

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

541 
publisher=Springer, 

542 
series=LNCS, 

543 
note={To appear}} 

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

545 

546 
and 

547 

548 
@inproceedings{MuellerNipkow, 

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

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

551 
booktitle={Proc.\ TACAS Workshop}, 

552 
organization={Aarhus University, BRICS report}, 

553 
year=1995} 

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

555 
*} 

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

556 
options [document = false] 
48481  557 
theories Solve 
558 

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

559 
session "HOLLattice" in Lattice = HOL + 
48481  560 
description {* 
561 
Author: Markus Wenzel, TU Muenchen 

562 

563 
Basic theory of lattices and orders. 

564 
*} 

565 
theories CompleteLattice 

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

566 
document_files "root.tex" 
48481  567 

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

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

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

571 
*} 
65548  572 
options [document = false] 
65543  573 
sessions 
574 
"HOLNumber_Theory" 

65548  575 
theories 
57507  576 
Adhoc_Overloading_Examples 
48481  577 
Antiquote 
65549  578 
Argo_Examples 
579 
Arith_Examples 

580 
Ballot 

581 
BinEx 

582 
Birthday_Paradox 

583 
Bubblesort 

584 
CTL 

585 
Cartouche_Examples 

65563  586 
Case_Product 
65549  587 
Chinese 
588 
Classical 

589 
Code_Binary_Nat_examples 

590 
Code_Timing 

591 
Coercion_Examples 

592 
Coherent 

593 
Commands 

594 
Computations 

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

595 
Cubic_Quartic 
65549  596 
Dedekind_Real 
597 
Erdoes_Szekeres 

598 
Eval_Examples 

599 
Executable_Relation 

600 
Execute_Choice 

601 
Functions 

602 
Gauge_Integration 

603 
Groebner_Examples 

604 
Guess 

605 
HarmonicSeries 

606 
Hebrew 

607 
Hex_Bin_Examples 

608 
IArray_Examples 

609 
Iff_Oracle 

610 
Induction_Schema 

48481  611 
Intuitionistic 
65549  612 
Lagrange 
613 
List_to_Set_Comprehension_Examples 

614 
LocaleTest2 

615 
ML 

48481  616 
MergeSort 
65549  617 
MonoidGroup 
618 
Multiquote 

619 
NatSum 

620 
Normalization_by_Evaluation 

621 
PER 

622 
Parallel_Example 

623 
Peano_Axioms 

624 
Perm_Fragments 

625 
PresburgerEx 

48481  626 
Primrec 
65549  627 
Pythagoras 
628 
Quicksort 

629 
Records 

630 
Reflection_Examples 

631 
Refute_Examples 

632 
Rewrite_Examples 

633 
SAT_Examples 

634 
SOS 

635 
SOS_Cert 

636 
Seq 

637 
Serbian 

638 
Set_Comprehension_Pointfree_Examples 

48481  639 
Set_Theory 
65549  640 
Simproc_Tests 
641 
Simps_Case_Conv_Examples 

48481  642 
Sqrt 
643 
Sqrt_Script 

65549  644 
Sudoku 
645 
Sum_of_Powers 

646 
Tarski 

647 
Termination 

648 
ThreeDivides 

61368  649 
Transfer_Debug 
48481  650 
Transfer_Ex 
651 
Transfer_Int_Nat 

56922  652 
Transitive_Closure_Table_Ex 
65549  653 
Tree23 
654 
Unification 

655 
While_Combinator_Example 

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

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

657 
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

658 
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

659 
Meson_Test 
48481  660 

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

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

662 
description {* 
61935  663 
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

664 
*} 
61939  665 
options [quick_and_dirty] 
48481  666 
theories [document = false] 
667 
"~~/src/HOL/Library/Lattice_Syntax" 

65417  668 
"../Computational_Algebra/Primes" 
48481  669 
theories 
61939  670 
Knaster_Tarski 
671 
Peirce 

672 
Drinker 

48481  673 
Cantor 
61939  674 
Structured_Statements 
675 
Basic_Logic 

48481  676 
Expr_Compiler 
677 
Fibonacci 

678 
Group 

679 
Group_Context 

680 
Group_Notepad 

681 
Hoare_Ex 

682 
Mutilated_Checkerboard 

683 
Puzzle 

684 
Summation 

61935  685 
First_Order_Logic 
686 
Higher_Order_Logic 

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

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

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

689 
"root.tex" 
48481  690 

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

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

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

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

694 
*} 
66444  695 
sessions 
696 
FOL 

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

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

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

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

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

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

702 

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

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

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

705 
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

706 
*} 
65543  707 
theories [document = false] 
708 
"~~/src/HOL/Library/Nat_Bijection" 

709 
theories 

710 
SET_Protocol 

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

711 
document_files "root.tex" 
48481  712 

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

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

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

715 
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

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

718 
document_files "root.tex" 
48481  719 

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

720 
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

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

722 
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

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

724 
options [document = false] 
48481  725 
theories TLA 
726 

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

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

728 
options [document = false] 
48481  729 
theories Inc 
730 

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

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

732 
options [document = false] 
48481  733 
theories DBuffer 
734 

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

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

736 
options [document = false] 
48481  737 
theories MemoryImplementation 
738 

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

739 
session "HOLTPTP" in TPTP = "HOLLibrary" + 
48481  740 
description {* 
741 
Author: Jasmin Blanchette, TU Muenchen 

742 
Author: Nik Sultana, University of Cambridge 

743 
Copyright 2011 

744 

745 
TPTPrelated extensions. 

746 
*} 

62354  747 
options [document = false] 
48481  748 
theories 
749 
ATP_Theory_Export 

750 
MaSh_Eval 

751 
TPTP_Interpret 

752 
THF_Arith 

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

753 
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

754 
theories 
48481  755 
ATP_Problem_Import 
756 

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

760 
"~~/src/HOL/Library/Permutation" 

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

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

766 
document_files "root.tex" 
48481  767 

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

768 
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

769 
theories 
65538  770 
Dining_Cryptographers 
771 
Koepf_Duermuth_Countermeasure 

772 
Measure_Not_CCC 

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

773 

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

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

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

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

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

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

779 
Nominal 
48481  780 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

805 
VC_Condition 
48481  806 

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

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

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

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

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

811 
options [document = false] 
59747  812 
theories 
813 
Cardinals 

814 
Bounded_Set 

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

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

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

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

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

819 

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

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

821 
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

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

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

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

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

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

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

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

831 
"Derivation_Trees/Parallel_Composition" 
50517  832 
Koenig 
60921  833 
Lift_BNF 
61745  834 
Milner_Tofte 
54961  835 
Stream_Processor 
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset

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

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

840 

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

841 
session "HOLCorec_Examples" (timing) in Corec_Examples = "HOLLibrary" + 
62694  842 
description {* 
843 
Corecursion Examples. 

844 
*} 

845 
options [document = false] 

846 
theories 

847 
LFilter 

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

851 
"Tests/Iterate_GPV" 
62696  852 
theories [quick_and_dirty] 
853 
"Tests/GPV_Bare_Bones" 

854 
"Tests/Merge_D" 

855 
"Tests/Merge_Poly" 

856 
"Tests/Misc_Mono" 

857 
"Tests/Misc_Poly" 

858 
"Tests/Small_Concrete" 

62725  859 
"Tests/Stream_Friends" 
62696  860 
"Tests/TLList_Friends" 
63190  861 
"Tests/Type_Class" 
62694  862 

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

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

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

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

867 
Word 
66445  868 
WordBitwise 
66443  869 
Bit_Comparison 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

870 
document_files "root.bib" "root.tex" 
48481  871 

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

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

873 
options [document = false] 
48481  874 
theories WordExamples 
875 

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

876 
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

877 
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

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

879 
document_files "root.tex" 
48481  880 

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

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

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

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

884 
*} 
62479  885 
theories 
886 
Nonstandard_Analysis 

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

887 
document_files "root.tex" 
48481  888 

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

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

890 
options [document = false] 
65543  891 
theories 
892 
NSPrimes 

48481  893 

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

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

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

897 

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

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

900 
theories Ex 
48481  901 

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

902 
session "HOLWordSMT_Examples" (timing) in SMT_Examples = "HOLWord" + 
62354  903 
options [document = false, quick_and_dirty] 
48481  904 
theories 
52722  905 
Boogie 
48481  906 
SMT_Examples 
907 
SMT_Word_Examples 

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

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

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

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

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

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

914 
"VCC_Max.certs" 
48481  915 

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

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

917 
options [document = false] 
65382  918 
theories 
919 
SPARK (global) 

48481  920 

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

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

922 
options [document = false, spark_prv = false] 
48481  923 
theories 
924 
"Gcd/Greatest_Common_Divisor" 

925 

926 
"Liseq/Longest_Increasing_Subsequence" 

927 

928 
"RIPEMD160/F" 

929 
"RIPEMD160/Hash" 

930 
"RIPEMD160/K_L" 

931 
"RIPEMD160/K_R" 

932 
"RIPEMD160/R_L" 

933 
"RIPEMD160/Round" 

934 
"RIPEMD160/R_R" 

935 
"RIPEMD160/S_L" 

936 
"RIPEMD160/S_R" 

937 

938 
"Sqrt/Sqrt" 

939 
files 

940 
"Gcd/greatest_common_divisor/g_c_d.fdl" 

941 
"Gcd/greatest_common_divisor/g_c_d.rls" 

942 
"Gcd/greatest_common_divisor/g_c_d.siv" 

943 
"Liseq/liseq/liseq_length.fdl" 

944 
"Liseq/liseq/liseq_length.rls" 

945 
"Liseq/liseq/liseq_length.siv" 

946 
"RIPEMD160/rmd/f.fdl" 

947 
"RIPEMD160/rmd/f.rls" 

948 
"RIPEMD160/rmd/f.siv" 

949 
"RIPEMD160/rmd/hash.fdl" 

950 
"RIPEMD160/rmd/hash.rls" 

951 
"RIPEMD160/rmd/hash.siv" 

952 
"RIPEMD160/rmd/k_l.fdl" 

953 
"RIPEMD160/rmd/k_l.rls" 

954 
"RIPEMD160/rmd/k_l.siv" 

955 
"RIPEMD160/rmd/k_r.fdl" 

956 
"RIPEMD160/rmd/k_r.rls" 

957 
"RIPEMD160/rmd/k_r.siv" 

958 
"RIPEMD160/rmd/r_l.fdl" 

959 
"RIPEMD160/rmd/r_l.rls" 

960 
"RIPEMD160/rmd/r_l.siv" 

961 
"RIPEMD160/rmd/round.fdl" 

962 
"RIPEMD160/rmd/round.rls" 

963 
"RIPEMD160/rmd/round.siv" 

964 
"RIPEMD160/rmd/r_r.fdl" 

965 
"RIPEMD160/rmd/r_r.rls" 

966 
"RIPEMD160/rmd/r_r.siv" 

967 
"RIPEMD160/rmd/s_l.fdl" 

968 
"RIPEMD160/rmd/s_l.rls" 

969 
"RIPEMD160/rmd/s_l.siv" 

970 
"RIPEMD160/rmd/s_r.fdl" 

971 
"RIPEMD160/rmd/s_r.rls" 

972 
"RIPEMD160/rmd/s_r.siv" 

973 

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

975 
options [show_question_marks = false, spark_prv = false] 
66031  976 
sessions 
977 
"HOLSPARKExamples" 

48481  978 
theories 
979 
Example_Verification 

980 
VC_Principles 

981 
Reference 

982 
Complex_Types 

983 
files 

984 
"complex_types_app/initialize.fdl" 

985 
"complex_types_app/initialize.rls" 

986 
"complex_types_app/initialize.siv" 

987 
"loop_invariant/proc1.fdl" 

988 
"loop_invariant/proc1.rls" 

989 
"loop_invariant/proc1.siv" 

990 
"loop_invariant/proc2.fdl" 

991 
"loop_invariant/proc2.rls" 

992 
"loop_invariant/proc2.siv" 

993 
"simple_greatest_common_divisor/g_c_d.fdl" 

994 
"simple_greatest_common_divisor/g_c_d.rls" 

995 
"simple_greatest_common_divisor/g_c_d.siv" 

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

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

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

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

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

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

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

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

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

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

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

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

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

1008 
"Simple_Gcd.ads" 
48481  1009 

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

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

1011 
options [document = false] 
48481  1012 
theories MutabelleExtra 
1013 

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

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

1015 
options [document = false] 
48588  1016 
theories 
48690  1017 
Quickcheck_Examples 
1018 
Quickcheck_Lattice_Examples 

1019 
Completeness 

1020 
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

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

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

1023 
Hotel_Example 
48598  1024 
Quickcheck_Narrowing_Examples 
48588  1025 

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

1026 
session "HOLQuotient_Examples" (timing) in Quotient_Examples = "HOLAlgebra" + 
48481  1027 
description {* 
1028 
Author: Cezary Kaliszyk and Christian Urban 

1029 
*} 

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

1030 
options [document = false] 
48481  1031 
theories 
1032 
DList 

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

1033 
Quotient_FSet 
48481  1034 
Quotient_Int 
1035 
Quotient_Message 

1036 
Lift_FSet 

1037 
Lift_Set 

1038 
Lift_Fun 

1039 
Quotient_Rat 

1040 
Lift_DList 

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

1041 
Int_Pow 
60237  1042 
Lifting_Code_Dt_Test 
48481  1043 

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

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

1045 
options [document = false] 
62354  1046 
theories 
48481  1047 
Examples 
1048 
Predicate_Compile_Tests 

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

1049 
Predicate_Compile_Quickcheck_Examples 
48481  1050 
Specialisation_Examples 
48690  1051 
IMP_1 
1052 
IMP_2 

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

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

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

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

1057 
theories [condition = ISABELLE_SWIPL] 
48690  1058 
Code_Prolog_Examples 
1059 
Context_Free_Grammar_Example 

1060 
Hotel_Example_Prolog 

1061 
Lambda_Example 

1062 
List_Examples 

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

1063 
theories [condition = ISABELLE_SWIPL, quick_and_dirty] 
48690  1064 
Reg_Exp_Example 
48481  1065 

64551  1066 
session "HOLTypes_To_Sets" in Types_To_Sets = HOL + 
1067 
description {* 

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

1069 
*} 

1070 
options [document = false] 

1071 
theories 

1072 
Types_To_Sets 

1073 
"Examples/Prerequisites" 

1074 
"Examples/Finite" 

1075 
"Examples/T2_Spaces" 

1076 

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

1077 
session HOLCF (main timing) in HOLCF = HOL + 
48338  1078 
description {* 
1079 
Author: Franz Regensburger 

1080 
Author: Brian Huffman 

1081 

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

1083 
*} 

65543  1084 
sessions 
1085 
"HOLLibrary" 

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

1086 
theories [document = false] 
48338  1087 
"~~/src/HOL/Library/Nat_Bijection" 
1088 
"~~/src/HOL/Library/Countable" 

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

1091 
document_files "root.tex" 
48481  1092 

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

1093 
session "HOLCFTutorial" in "HOLCF/Tutorial" = HOLCF + 
48481  1094 
theories 
1095 
Domain_ex 

1096 
Fixrec_ex 

1097 
New_Domain 

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

1098 
document_files "root.tex" 
48481  1099 

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

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

1101 
options [document = false] 
65570  1102 
theories 
1103 
HOLCF_Library 

1104 
HOL_Cpo 

48481  1105 

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

1106 
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

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

1108 
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

1109 

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

1110 
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

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

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

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

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

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

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

1117 
document_files "root.tex" 
48338  1118 

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

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

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

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

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

1123 
options [document = false] 
48481  1124 
theories 
1125 
Dnat 

1126 
Dagstuhl 

1127 
Focus_ex 

1128 
Fix2 

1129 
Hoare 

1130 
Concurrency_Monad 

1131 
Loop 

1132 
Powerdomain_ex 

1133 
Domain_Proofs 

1134 
Letrec 

1135 
Pattern_Match 

1136 

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

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

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

1139 
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

1140 

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

1141 
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

1142 

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

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

1144 
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

1145 

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

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

1147 
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

1148 

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

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

1150 
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

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

1152 
options [document = false] 
48481  1153 
theories 
1154 
Fstreams 

1155 
FOCUS 

1156 
Buffer_adm 

1157 

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

1158 
session IOA (timing) in "HOLCF/IOA" = HOLCF + 
48481  1159 
description {* 
1160 
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

1161 
Copyright 1997 TU München 
48481  1162 

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

1163 
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

1164 

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

1165 
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

1166 
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

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

1169 
options [document = false] 
65538  1170 
theories Abstraction 
48481  1171 

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

1172 
session "IOAABP" in "HOLCF/IOA/ABP" = IOA + 
48481  1173 
description {* 
1174 
Author: Olaf Mueller 

1175 

1176 
The Alternating Bit Protocol performed in I/OAutomata. 

1177 
*} 

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

1178 
options [document = false] 
59503  1179 
theories 
1180 
Correctness 

1181 
Spec 

48481  1182 

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

1183 
session "IOANTP" in "HOLCF/IOA/NTP" = IOA + 
48481  1184 
description {* 
1185 
Author: Tobias Nipkow & Konrad Slind 

1186 

1187 
A network transmission protocol, performed in the 

1188 
I/O automata formalization by Olaf Mueller. 

1189 
*} 

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

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

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

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

1196 

1197 
Memory storage case study. 

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 "IOAex" in "HOLCF/IOA/ex" = IOA + 
48481  1203 
description {* 
1204 
Author: Olaf Mueller 

1205 
*} 

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

1206 
options [document = false] 
48481  1207 
theories 
1208 
TrivEx 

1209 
TrivEx2 