author  wenzelm 
Wed, 19 Apr 2017 15:53:58 +0200  
changeset 65509  ffedb16f382f 
parent 65485  8c7bc3a13513 
child 65515  f595b7532dc9 
child 65530  09c00a304c00 
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] 
65509
ffedb16f382f
clarified session structure: avoid ambiguity of file ~~/src/HOL/Library/Old_Datatype.thy;
wenzelm
parents:
65485
diff
changeset

23 
sessions "HOLLibrary" 
ffedb16f382f
clarified session structure: avoid ambiguity of file ~~/src/HOL/Library/Old_Datatype.thy;
wenzelm
parents:
65485
diff
changeset

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

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

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

27 
"Tools/Quickcheck/PNF_Narrowing_Engine.hs" 
48338  28 

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

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

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

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

32 
*} 
48481  33 
theories 
34 
Library 

64588  35 
(*conflicting type class instantiations and dependent applications*) 
36 
Finite_Lattice 

37 
List_lexord 

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

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

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

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

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

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

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

45 
Code_Char 
55447  46 
Code_Prolog 
48481  47 
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

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

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

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

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

52 
RBT_Set 
64588  53 
(*prototypic tools*) 
54 
Predicate_Compile_Quickcheck 

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

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

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

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

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

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

65375  62 
session "HOLAnalysis" (main timing) in Analysis = HOL + 
63 
theories 

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

64 
Analysis 
65375  65 
document_files 
66 
"root.tex" 

67 

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

69 
theories 

70 
Approximations 

71 
Circle_Area 

72 

65485  73 
session "HOLComputational_Algebra" in "Computational_Algebra" = HOL + 
65417  74 
theories 
75 
Computational_Algebra 

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

77 
Field_as_Ring 

78 
Polynomial_Factorial 

79 

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

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

83 

84 
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

85 

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

86 
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

87 
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

88 
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

89 
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

90 

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

91 
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

92 
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

93 

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

94 
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

95 
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

96 
continous linearform on the whole vectorspace. 
48481  97 
*} 
98 
theories Hahn_Banach 

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

99 
document_files "root.bib" "root.tex" 
48481  100 

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

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

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

103 
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

104 

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

105 
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

106 
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

107 

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

108 
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

109 
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

110 

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

111 
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

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

113 
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

114 

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

115 
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

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

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

118 
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

119 
"~~/src/HOL/Library/Old_Datatype" 
48481  120 
theories [quick_and_dirty] 
121 
Common_Patterns 

122 
theories 

61935  123 
Nested_Datatype 
48481  124 
QuoDataType 
125 
QuoNestedDataType 

126 
Term 

127 
SList 

128 
ABexp 

129 
Tree 

130 
Ordinals 

131 
Sigma_Algebra 

132 
Comb 

133 
PropLog 

134 
Com 

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

135 
document_files "root.tex" 
48481  136 

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

137 
session "HOLIMP" (timing) in IMP = HOL + 
59446  138 
options [document_variants = document] 
48481  139 
theories [document = false] 
140 
"~~/src/HOL/Library/While_Combinator" 

141 
"~~/src/HOL/Library/Char_ord" 

142 
"~~/src/HOL/Library/List_lexord" 

51625  143 
"~~/src/HOL/Library/Quotient_List" 
144 
"~~/src/HOL/Library/Extended" 

48481  145 
theories 
146 
BExp 

147 
ASM 

50050  148 
Finite_Reachable 
52394  149 
Denotational 
52400  150 
Compiler2 
48481  151 
Poly_Types 
152 
Sec_Typing 

153 
Sec_TypingT 

52726  154 
Def_Init_Big 
155 
Def_Init_Small 

156 
Fold 

48481  157 
Live 
158 
Live_True 

159 
Hoare_Examples 

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

160 
Hoare_Sound_Complete 
52269  161 
VCG 
52282  162 
Hoare_Total 
63538
d7b5e2a222c2
added new vcg based on existentially quantified whilerule
nipkow
parents:
63537
diff
changeset

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

165 
Collecting_Examples 
48481  166 
Abs_Int_Tests 
167 
Abs_Int1_parity 

168 
Abs_Int1_const 

169 
Abs_Int3 

170 
Procs_Dyn_Vars_Dyn 

171 
Procs_Stat_Vars_Dyn 

172 
Procs_Stat_Vars_Stat 

173 
C_like 

174 
OO 

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

175 
document_files "root.bib" "root.tex" 
48481  176 

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

177 
session "HOLIMPP" in IMPP = HOL + 
48481  178 
description {* 
179 
Author: David von Oheimb 

180 
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

181 

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

182 
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

183 

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

184 
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

185 
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

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

188 
options [document = false] 
48481  189 
theories EvenOdd 
190 

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

191 
session "HOLData_Structures" (timing) in Data_Structures = HOL + 
61203  192 
options [document_variants = document] 
193 
theories [document = false] 

194 
"Less_False" 

62706  195 
"~~/src/HOL/Library/Multiset" 
64323  196 
"~~/src/HOL/Number_Theory/Fib" 
61203  197 
theories 
63829  198 
Balance 
61203  199 
Tree_Map 
61232  200 
AVL_Map 
61224  201 
RBT_Map 
61469
cd82b1023932
added 23 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
61368
diff
changeset

202 
Tree23_Map 
61514  203 
Tree234_Map 
61789  204 
Brother12_Map 
62130  205 
AA_Map 
61525  206 
Splay_Map 
62706  207 
Leftist_Heap 
61224  208 
document_files "root.tex" "root.bib" 
61203  209 

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

210 
session "HOLImport" in Import = HOL + 
48481  211 
theories HOL_Light_Maps 
212 
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 

213 

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

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

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

216 
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

217 
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

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

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

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

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

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

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

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

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

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

227 
"root.tex" 
48481  228 

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

229 
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

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

231 
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

232 
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

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

235 
document_files "root.bib" "root.tex" 
48481  236 

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

237 
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

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

239 
Verification of 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

262 
Code_Test_SMLNJ 
48481  263 

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

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

267 
Author: Jasmin Blanchette, TU Muenchen 

268 

269 
Testing Metis and Sledgehammer. 

270 
*} 

58423  271 
options [document = false] 
48481  272 
theories 
273 
Abstraction 

274 
Big_O 

275 
Binary_Tree 

276 
Clausification 

277 
Message 

278 
Proxies 

279 
Tarski 

280 
Trans_Closure 

281 
Sets 

282 

55072  283 
session "HOLNitpick_Examples" in Nitpick_Examples = HOL + 
48481  284 
description {* 
285 
Author: Jasmin Blanchette, TU Muenchen 

286 
Copyright 2009 

287 
*} 

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

288 
options [document = false] 
48481  289 
theories [quick_and_dirty] Nitpick_Examples 
290 

64389  291 
session "HOLNunchaku" in Nunchaku = HOL + 
292 
description {* 

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

294 
Copyright 2015, 2016 

295 

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

297 
*} 

298 
options [document = false] 

299 
theories Nunchaku 

300 

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

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

304 

305 
The Isabelle Algebraic Library. 

306 
*} 

307 
theories [document = false] 

308 
(* Preliminaries from set and number theory *) 

309 
"~~/src/HOL/Library/FuncSet" 

65417  310 
"~~/src/HOL/Computational_Algebra/Primes" 
48481  311 
"~~/src/HOL/Library/Permutation" 
312 
theories 

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

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

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

315 

48481  316 
(* Groups *) 
317 
FiniteProduct (* Product operator for commutative groups *) 

318 
Sylow (* Sylow's theorem *) 

319 
Bij (* Automorphism Groups *) 

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

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

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

322 
Multiplicative_Group 
48481  323 

324 
(* Rings *) 

325 
Divisibility (* Rings *) 

326 
IntRing (* Ideals and residue classes *) 

327 
UnivPoly (* Polynomials *) 

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

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

329 
document_files "root.bib" "root.tex" 
48481  330 

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

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

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

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

334 
*} 
48481  335 
theories 
336 
Auth_Shared 

337 
Auth_Public 

338 
"Smartcard/Auth_Smartcard" 

339 
"Guard/Auth_Guard_Shared" 

340 
"Guard/Auth_Guard_Public" 

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

341 
document_files "root.tex" 
48481  342 

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

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

346 
Copyright 1998 University of Cambridge 

347 

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

348 
Verifying security protocols using Chandy and Misra's UNITY formalism. 
48481  349 
*} 
350 
theories 

351 
(*Basic metatheory*) 

352 
"UNITY_Main" 

353 

354 
(*Simple examples: no composition*) 

355 
"Simple/Deadlock" 

356 
"Simple/Common" 

357 
"Simple/Network" 

358 
"Simple/Token" 

359 
"Simple/Channel" 

360 
"Simple/Lift" 

361 
"Simple/Mutex" 

362 
"Simple/Reach" 

363 
"Simple/Reachability" 

364 

365 
(*Verifying security protocols using UNITY*) 

366 
"Simple/NSP_Bad" 

367 

368 
(*Example of composition*) 

369 
"Comp/Handshake" 

370 

371 
(*Universal properties examples*) 

372 
"Comp/Counter" 

373 
"Comp/Counterc" 

374 
"Comp/Priority" 

375 

376 
"Comp/TimerArray" 

377 
"Comp/Progress" 

378 

379 
"Comp/Alloc" 

380 
"Comp/AllocImpl" 

381 
"Comp/Client" 

382 

383 
(*obsolete*) 

384 
"ELT" 

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

385 
document_files "root.tex" 
48481  386 

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

387 
session "HOLUnix" in Unix = HOL + 
48481  388 
options [print_mode = "no_brackets,no_type_brackets"] 
389 
theories Unix 

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

390 
document_files "root.bib" "root.tex" 
48481  391 

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

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

394 
document_files "root.tex" 
48481  395 

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

396 
session "HOLImperative_HOL" in Imperative_HOL = HOL + 
59446  397 
options [print_mode = "iff,no_brackets"] 
48481  398 
theories [document = false] 
399 
"~~/src/HOL/Library/Countable" 

400 
"~~/src/HOL/Library/Monad_Syntax" 

401 
"~~/src/HOL/Library/LaTeXsugar" 

402 
theories Imperative_HOL_ex 

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

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

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

405 
session "HOLDecision_Procs" (timing) in Decision_Procs = HOL + 
51544  406 
description {* 
407 
Various decision procedures, typically involving reflection. 

408 
*} 

62354  409 
options [document = false] 
48481  410 
theories Decision_Procs 
411 

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

412 
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

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

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

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

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

417 
XML_Data 
48481  418 

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

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

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

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

422 
*} 
62354  423 
options [parallel_proofs = 0, quick_and_dirty = false] 
48481  424 
theories [document = false] 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51115
diff
changeset

425 
"~~/src/HOL/Library/Code_Target_Numeral" 
48481  426 
"~~/src/HOL/Library/Monad_Syntax" 
65417  427 
"~~/src/HOL/Computational_Algebra/Primes" 
48481  428 
"~~/src/HOL/Library/State_Monad" 
429 
theories 

430 
Greatest_Common_Divisor 

431 
Warshall 

432 
Higman_Extraction 

433 
Pigeonhole 

434 
Euclid 

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

435 
document_files "root.bib" "root.tex" 
48481  436 

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

437 
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

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

439 
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

440 

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

441 
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

442 
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

443 

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

444 
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

445 
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

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

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

450 
"~~/src/HOL/Library/Code_Target_Int" 
48481  451 
theories 
452 
Eta 

453 
StrongNorm 

454 
Standardization 

455 
WeakNorm 

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

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

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

458 
session "HOLProlog" in Prolog = HOL + 
48481  459 
description {* 
460 
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

461 

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

462 
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

463 

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

464 
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

465 
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

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

468 
options [document = false] 
48481  469 
theories Test Type 
470 

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

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

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

473 
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

474 
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

475 
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

476 
*} 
59446  477 
theories [document = false] 
478 
"~~/src/HOL/Library/While_Combinator" 

479 
theories 

480 
MicroJava 

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

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

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

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

484 
"root.tex" 
48481  485 

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

486 
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

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

488 
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

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

491 
document_files "root.bib" "root.tex" 
48481  492 

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

493 
session "HOLBali" (timing) in Bali = HOL + 
48481  494 
theories 
495 
AxExample 

496 
AxSound 

497 
AxCompl 

498 
Trans 

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

500 
document_files "root.tex" 
48481  501 

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

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

504 
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

505 
Copyright 19941996 TU Muenchen 
48481  506 

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

507 
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

508 
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

509 
proofs of two communication protocols which formerly have been here. 
48481  510 

511 
@inproceedings{NipkowSlindIOA, 

512 
author={Tobias Nipkow and Konrad Slind}, 

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

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

515 
publisher=Springer, 

516 
series=LNCS, 

517 
note={To appear}} 

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

519 

520 
and 

521 

522 
@inproceedings{MuellerNipkow, 

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

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

525 
booktitle={Proc.\ TACAS Workshop}, 

526 
organization={Aarhus University, BRICS report}, 

527 
year=1995} 

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

529 
*} 

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

530 
options [document = false] 
48481  531 
theories Solve 
532 

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

533 
session "HOLLattice" in Lattice = HOL + 
48481  534 
description {* 
535 
Author: Markus Wenzel, TU Muenchen 

536 

537 
Basic theory of lattices and orders. 

538 
*} 

539 
theories CompleteLattice 

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

540 
document_files "root.tex" 
48481  541 

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

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

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

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

545 
*} 
48481  546 
theories [document = false] 
547 
"~~/src/HOL/Library/State_Monad" 

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

548 
Code_Binary_Nat_examples 
48481  549 
"~~/src/HOL/Library/FuncSet" 
550 
Eval_Examples 

551 
Normalization_by_Evaluation 

552 
Hebrew 

553 
Chinese 

554 
Serbian 

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

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

557 
Cartouche_Examples 
64959  558 
Computations 
48481  559 
theories 
59090  560 
Commands 
57507  561 
Adhoc_Overloading_Examples 
48481  562 
Iff_Oracle 
563 
Coercion_Examples 

64920  564 
Peano_Axioms 
48481  565 
Guess 
62999  566 
Functions 
48481  567 
Induction_Schema 
568 
LocaleTest2 

569 
Records 

570 
While_Combinator_Example 

571 
MonoidGroup 

572 
BinEx 

573 
Hex_Bin_Examples 

574 
Antiquote 

575 
Multiquote 

576 
PER 

577 
NatSum 

578 
ThreeDivides 

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

579 
Cubic_Quartic 
59739  580 
Pythagoras 
48481  581 
Intuitionistic 
582 
CTL 

583 
Arith_Examples 

584 
Tree23 

58644  585 
Bubblesort 
48481  586 
MergeSort 
587 
Lagrange 

588 
Groebner_Examples 

589 
Unification 

590 
Primrec 

591 
Tarski 

592 
Classical 

593 
Set_Theory 

594 
Termination 

595 
Coherent 

596 
PresburgerEx 

51093  597 
Reflection_Examples 
48481  598 
Sqrt 
599 
Sqrt_Script 

61368  600 
Transfer_Debug 
48481  601 
Transfer_Ex 
602 
Transfer_Int_Nat 

56922  603 
Transitive_Closure_Table_Ex 
48481  604 
HarmonicSeries 
605 
Refute_Examples 

606 
Execute_Choice 

607 
Gauge_Integration 

608 
Dedekind_Real 

609 
Quicksort 

610 
Birthday_Paradox 

611 
List_to_Set_Comprehension_Examples 

612 
Seq 

613 
Simproc_Tests 

614 
Executable_Relation 

55663  615 
Set_Comprehension_Pointfree_Examples 
48481  616 
Parallel_Example 
50138  617 
IArray_Examples 
53430  618 
Simps_Case_Conv_Examples 
53935  619 
ML 
59739  620 
Rewrite_Examples 
56815  621 
SAT_Examples 
58630  622 
SOS 
58418  623 
SOS_Cert 
60603
09ecbd791d4a
add examples from Freek's top 100 theorems (thms 30, 73, 77)
bulwahn
parents:
60470
diff
changeset

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

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

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

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

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

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

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

632 
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

633 
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

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

635 
document_files "root.bib" "root.tex" 
48481  636 

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

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

638 
description {* 
61935  639 
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

640 
*} 
61939  641 
options [quick_and_dirty] 
48481  642 
theories [document = false] 
643 
"~~/src/HOL/Library/Lattice_Syntax" 

65417  644 
"../Computational_Algebra/Primes" 
48481  645 
theories 
61939  646 
Knaster_Tarski 
647 
Peirce 

648 
Drinker 

48481  649 
Cantor 
61939  650 
Structured_Statements 
651 
Basic_Logic 

48481  652 
Expr_Compiler 
653 
Fibonacci 

654 
Group 

655 
Group_Context 

656 
Group_Notepad 

657 
Hoare_Ex 

658 
Mutilated_Checkerboard 

659 
Puzzle 

660 
Summation 

61935  661 
First_Order_Logic 
662 
Higher_Order_Logic 

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

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

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

665 
"root.tex" 
48481  666 

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

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

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

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

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

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

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

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

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

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

676 

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

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

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

679 
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

680 
*} 
48481  681 
theories [document = false] "~~/src/HOL/Library/Nat_Bijection" 
682 
theories SET_Protocol 

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

683 
document_files "root.tex" 
48481  684 

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

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

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

687 
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

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

690 
document_files "root.tex" 
48481  691 

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

692 
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

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

694 
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

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

696 
options [document = false] 
48481  697 
theories TLA 
698 

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

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

700 
options [document = false] 
48481  701 
theories Inc 
702 

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

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

704 
options [document = false] 
48481  705 
theories DBuffer 
706 

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

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

708 
options [document = false] 
48481  709 
theories MemoryImplementation 
710 

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

711 
session "HOLTPTP" in TPTP = HOL + 
48481  712 
description {* 
713 
Author: Jasmin Blanchette, TU Muenchen 

714 
Author: Nik Sultana, University of Cambridge 

715 
Copyright 2011 

716 

717 
TPTPrelated extensions. 

718 
*} 

62354  719 
options [document = false] 
48481  720 
theories 
721 
ATP_Theory_Export 

722 
MaSh_Eval 

723 
TPTP_Interpret 

724 
THF_Arith 

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

725 
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

726 
theories 
48481  727 
ATP_Problem_Import 
728 

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

732 
"~~/src/HOL/Library/Permutation" 

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

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

738 
document_files "root.tex" 
48481  739 

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

740 
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

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

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

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

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

745 

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

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

747 
options [document = false] 
48481  748 
theories Nominal 
749 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

774 
VC_Condition 
48481  775 

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

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

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

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

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

780 
options [document = false] 
59747  781 
theories 
782 
Cardinals 

783 
Bounded_Set 

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

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

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

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

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

788 

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

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

790 
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

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

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

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

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

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

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

798 
TreeFsetI 
49872  799 
"Derivation_Trees/Gram_Lang" 
800 
"Derivation_Trees/Parallel" 

50517  801 
Koenig 
60921  802 
Lift_BNF 
61745  803 
Milner_Tofte 
54961  804 
Stream_Processor 
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset

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

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

809 

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

810 
session "HOLCorec_Examples" (timing) in Corec_Examples = HOL + 
62694  811 
description {* 
812 
Corecursion Examples. 

813 
*} 

814 
options [document = false] 

815 
theories 

816 
LFilter 

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

820 
"Tests/Iterate_GPV" 
62696  821 
theories [quick_and_dirty] 
822 
"Tests/GPV_Bare_Bones" 

823 
"Tests/Merge_D" 

824 
"Tests/Merge_Poly" 

825 
"Tests/Misc_Mono" 

826 
"Tests/Misc_Poly" 

827 
"Tests/Small_Concrete" 

62725  828 
"Tests/Stream_Friends" 
62696  829 
"Tests/TLList_Friends" 
63190  830 
"Tests/Type_Class" 
62694  831 

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

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

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

835 
document_files "root.bib" "root.tex" 
48481  836 

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

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

838 
options [document = false] 
48481  839 
theories WordExamples 
840 

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

841 
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

842 
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

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

844 
document_files "root.tex" 
48481  845 

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

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

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

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

849 
*} 
62479  850 
theories 
851 
Nonstandard_Analysis 

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

852 
document_files "root.tex" 
48481  853 

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

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

855 
options [document = false] 
48481  856 
theories NSPrimes 
857 

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

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

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

861 

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

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

864 
theories Ex 
48481  865 

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

866 
session "HOLWordSMT_Examples" (timing) in SMT_Examples = "HOLWord" + 
62354  867 
options [document = false, quick_and_dirty] 
48481  868 
theories 
52722  869 
Boogie 
48481  870 
SMT_Examples 
871 
SMT_Word_Examples 

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

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

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

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

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

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

878 
"VCC_Max.certs" 
48481  879 

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

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

881 
options [document = false] 
65382  882 
theories 
883 
SPARK (global) 

48481  884 

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

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

886 
options [document = false, spark_prv = false] 
48481  887 
theories 
888 
"Gcd/Greatest_Common_Divisor" 

889 

890 
"Liseq/Longest_Increasing_Subsequence" 

891 

892 
"RIPEMD160/F" 

893 
"RIPEMD160/Hash" 

894 
"RIPEMD160/K_L" 

895 
"RIPEMD160/K_R" 

896 
"RIPEMD160/R_L" 

897 
"RIPEMD160/Round" 

898 
"RIPEMD160/R_R" 

899 
"RIPEMD160/S_L" 

900 
"RIPEMD160/S_R" 

901 

902 
"Sqrt/Sqrt" 

903 
files 

904 
"Gcd/greatest_common_divisor/g_c_d.fdl" 

905 
"Gcd/greatest_common_divisor/g_c_d.rls" 

906 
"Gcd/greatest_common_divisor/g_c_d.siv" 

907 
"Liseq/liseq/liseq_length.fdl" 

908 
"Liseq/liseq/liseq_length.rls" 

909 
"Liseq/liseq/liseq_length.siv" 

910 
"RIPEMD160/rmd/f.fdl" 

911 
"RIPEMD160/rmd/f.rls" 

912 
"RIPEMD160/rmd/f.siv" 

913 
"RIPEMD160/rmd/hash.fdl" 

914 
"RIPEMD160/rmd/hash.rls" 

915 
"RIPEMD160/rmd/hash.siv" 

916 
"RIPEMD160/rmd/k_l.fdl" 

917 
"RIPEMD160/rmd/k_l.rls" 

918 
"RIPEMD160/rmd/k_l.siv" 

919 
"RIPEMD160/rmd/k_r.fdl" 

920 
"RIPEMD160/rmd/k_r.rls" 

921 
"RIPEMD160/rmd/k_r.siv" 

922 
"RIPEMD160/rmd/r_l.fdl" 

923 
"RIPEMD160/rmd/r_l.rls" 

924 
"RIPEMD160/rmd/r_l.siv" 

925 
"RIPEMD160/rmd/round.fdl" 

926 
"RIPEMD160/rmd/round.rls" 

927 
"RIPEMD160/rmd/round.siv" 

928 
"RIPEMD160/rmd/r_r.fdl" 

929 
"RIPEMD160/rmd/r_r.rls" 

930 
"RIPEMD160/rmd/r_r.siv" 

931 
"RIPEMD160/rmd/s_l.fdl" 

932 
"RIPEMD160/rmd/s_l.rls" 

933 
"RIPEMD160/rmd/s_l.siv" 

934 
"RIPEMD160/rmd/s_r.fdl" 

935 
"RIPEMD160/rmd/s_r.rls" 

936 
"RIPEMD160/rmd/s_r.siv" 

937 

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

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

939 
options [show_question_marks = false, spark_prv = false] 
48481  940 
theories 
941 
Example_Verification 

942 
VC_Principles 

943 
Reference 

944 
Complex_Types 

945 
files 

946 
"complex_types_app/initialize.fdl" 

947 
"complex_types_app/initialize.rls" 

948 
"complex_types_app/initialize.siv" 

949 
"loop_invariant/proc1.fdl" 

950 
"loop_invariant/proc1.rls" 

951 
"loop_invariant/proc1.siv" 

952 
"loop_invariant/proc2.fdl" 

953 
"loop_invariant/proc2.rls" 

954 
"loop_invariant/proc2.siv" 

955 
"simple_greatest_common_divisor/g_c_d.fdl" 

956 
"simple_greatest_common_divisor/g_c_d.rls" 

957 
"simple_greatest_common_divisor/g_c_d.siv" 

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

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

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

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

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

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

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

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

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

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

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

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

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

970 
"Simple_Gcd.ads" 
48481  971 

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

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

973 
options [document = false] 
48481  974 
theories MutabelleExtra 
975 

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

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

977 
options [document = false] 
48588  978 
theories 
48690  979 
Quickcheck_Examples 
980 
Quickcheck_Lattice_Examples 

981 
Completeness 

982 
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

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

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

985 
Hotel_Example 
48598  986 
Quickcheck_Narrowing_Examples 
48588  987 

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

988 
session "HOLQuotient_Examples" (timing) in Quotient_Examples = HOL + 
48481  989 
description {* 
990 
Author: Cezary Kaliszyk and Christian Urban 

991 
*} 

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

992 
options [document = false] 
48481  993 
theories 
994 
DList 

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

995 
Quotient_FSet 
48481  996 
Quotient_Int 
997 
Quotient_Message 

998 
Lift_FSet 

999 
Lift_Set 

1000 
Lift_Fun 

1001 
Quotient_Rat 

1002 
Lift_DList 

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

1003 
Int_Pow 
60237  1004 
Lifting_Code_Dt_Test 
48481  1005 

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

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

1007 
options [document = false] 
62354  1008 
theories 
48481  1009 
Examples 
1010 
Predicate_Compile_Tests 

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

1011 
Predicate_Compile_Quickcheck_Examples 
48481  1012 
Specialisation_Examples 
48690  1013 
IMP_1 
1014 
IMP_2 

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

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

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

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

1019 
theories [condition = ISABELLE_SWIPL] 
48690  1020 
Code_Prolog_Examples 
1021 
Context_Free_Grammar_Example 

1022 
Hotel_Example_Prolog 

1023 
Lambda_Example 

1024 
List_Examples 

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

1025 
theories [condition = ISABELLE_SWIPL, quick_and_dirty] 
48690  1026 
Reg_Exp_Example 
48481  1027 

64551  1028 
session "HOLTypes_To_Sets" in Types_To_Sets = HOL + 
1029 
description {* 

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

1031 
*} 

1032 
options [document = false] 

1033 
theories 

1034 
Types_To_Sets 

1035 
"Examples/Prerequisites" 

1036 
"Examples/Finite" 

1037 
"Examples/T2_Spaces" 

1038 

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

1039 
session HOLCF (main timing) in HOLCF = HOL + 
48338  1040 
description {* 
1041 
Author: Franz Regensburger 

1042 
Author: Brian Huffman 

1043 

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

1045 
*} 

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

1046 
theories [document = false] 
48338  1047 
"~~/src/HOL/Library/Nat_Bijection" 
1048 
"~~/src/HOL/Library/Countable" 

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

1051 
document_files "root.tex" 
48481  1052 

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

1053 
session "HOLCFTutorial" in "HOLCF/Tutorial" = HOLCF + 
48481  1054 
theories 
1055 
Domain_ex 

1056 
Fixrec_ex 

1057 
New_Domain 

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

1058 
document_files "root.tex" 
48481  1059 

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

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

1061 
options [document = false] 
48481  1062 
theories HOLCF_Library 
1063 

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

1064 
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

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

1066 
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

1067 

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

1068 
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

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

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

1072 
document_files "root.tex" 
48338  1073 

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

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

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

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

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

1078 
options [document = false] 
48481  1079 
theories 
1080 
Dnat 

1081 
Dagstuhl 

1082 
Focus_ex 

1083 
Fix2 

1084 
Hoare 

1085 
Concurrency_Monad 

1086 
Loop 

1087 
Powerdomain_ex 

1088 
Domain_Proofs 

1089 
Letrec 

1090 
Pattern_Match 

1091 

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

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

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

1094 
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

1095 

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

1096 
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

1097 

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

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

1099 
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

1100 

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

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

1102 
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

1103 

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

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

1105 
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

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

1107 
options [document = false] 
48481  1108 
theories 
1109 
Fstreams 

1110 
FOCUS 

1111 
Buffer_adm 

1112 

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

1113 
session IOA (timing) in "HOLCF/IOA" = HOLCF + 
48481  1114 
description {* 
1115 
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

1116 
Copyright 1997 TU München 
48481  1117 

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

1118 
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

1119 

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

1120 
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

1121 
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

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

1124 
options [document = false] 
62008  1125 
theories "Abstraction" 
48481  1126 

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

1127 
session "IOAABP" in "HOLCF/IOA/ABP" = IOA + 
48481  1128 
description {* 
1129 
Author: Olaf Mueller 

1130 

1131 
The Alternating Bit Protocol performed in I/OAutomata. 

1132 
*} 

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

1133 
options [document = false] 
59503  1134 
theories 
1135 
Correctness 

1136 
Spec 

48481  1137 

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

1138 
session "IOANTP" in "HOLCF/IOA/NTP" = IOA + 
48481  1139 
description {* 
1140 
Author: Tobias Nipkow & Konrad Slind 

1141 

1142 
A network transmission protocol, performed in the 

1143 
I/O automata formalization by Olaf Mueller. 

1144 
*} 

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

1145 
options [document = false] 
48481  1146 
theories Correctness 
1147 

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

1148 
session "IOAStorage" in "HOLCF/IOA/Storage" = IOA + 
48481  1149 
description {* 
1150 
Author: Olaf Mueller 

1151 

1152 
Memory storage case study. 

1153 
*} 

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

1154 
options [document = false] 
48481  1155 
theories Correctness 
1156 

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

1157 
session "IOAex" in "HOLCF/IOA/ex" = IOA + 
48481  1158 
description {* 
1159 
Author: Olaf Mueller 

1160 
*} 

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

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

1164 
TrivEx2 