author  nipkow 
Sat, 05 Dec 2015 16:13:28 +0100  
changeset 61789  9ce1a397410a 
parent 61784  21b34a2269e5 
child 61793  4c9e1e5a240e 
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 
*} 
56801
8dd9df88f647
some support for sessionqualified theories: allow to refer to resources via qualified name instead of odd filesystem path;
wenzelm
parents:
56781
diff
changeset

7 
global_theories 
8dd9df88f647
some support for sessionqualified theories: allow to refer to resources via qualified name instead of odd filesystem path;
wenzelm
parents:
56781
diff
changeset

8 
Main 
8dd9df88f647
some support for sessionqualified theories: allow to refer to resources via qualified name instead of odd filesystem path;
wenzelm
parents:
56781
diff
changeset

9 
Complex_Main 
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 

61152  17 
session "HOLProofs" (slow) = 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 
*} 
59006
272d7fb92396
no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";
wenzelm
parents:
58849
diff
changeset

21 
options [document = false, quick_and_dirty = false] 
52488
cd65ee49a8ba
discontinued system option "proofs"  global state of Proofterm.proofs is persistently compiled into HOLProofs image;
wenzelm
parents:
52424
diff
changeset

22 
theories Proofs (*sequential change of global flag!*) 
58372
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOLProofs' because of the inductive realizer)
blanchet
parents:
58371
diff
changeset

23 
theories "~~/src/HOL/Library/Old_Datatype" 
48901
5e0455e29339
more basic file dependencies  no load command here;
wenzelm
parents:
48765
diff
changeset

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

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

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

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

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

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

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

31 
*} 
48481  32 
theories 
33 
Library 

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

35 
(*conflicting type class instantiations*) 
48481  36 
List_lexord 
37 
Sublist_Order 

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

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

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

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

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

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

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

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

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

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

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

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

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

52 
(*legacy tools*) 
49985
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49932
diff
changeset

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

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

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

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

57 
document_files "root.bib" "root.tex" 
48481  58 

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

59 
session "HOLHahn_Banach" in Hahn_Banach = HOL + 
48481  60 
description {* 
61 
Author: Gertrud Bauer, TU Munich 

62 

63 
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

64 

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

65 
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

66 
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

67 
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

68 
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

69 

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

70 
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

71 
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

72 

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

73 
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

74 
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

75 
continous linearform on the whole vectorspace. 
48481  76 
*} 
77 
theories Hahn_Banach 

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

78 
document_files "root.bib" "root.tex" 
48481  79 

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

80 
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

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

82 
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

83 

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

84 
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

85 
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

86 

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

87 
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

88 
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

89 

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

90 
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

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

92 
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

93 

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

94 
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

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

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

97 
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

98 
"~~/src/HOL/Library/Old_Datatype" 
48481  99 
theories [quick_and_dirty] 
100 
Common_Patterns 

101 
theories 

102 
QuoDataType 

103 
QuoNestedDataType 

104 
Term 

105 
SList 

106 
ABexp 

107 
Tree 

108 
Ordinals 

109 
Sigma_Algebra 

110 
Comb 

111 
PropLog 

112 
Com 

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

113 
document_files "root.tex" 
48481  114 

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

115 
session "HOLIMP" in IMP = HOL + 
59446  116 
options [document_variants = document] 
48481  117 
theories [document = false] 
118 
"~~/src/HOL/Library/While_Combinator" 

119 
"~~/src/HOL/Library/Char_ord" 

120 
"~~/src/HOL/Library/List_lexord" 

51625  121 
"~~/src/HOL/Library/Quotient_List" 
122 
"~~/src/HOL/Library/Extended" 

48481  123 
theories 
124 
BExp 

125 
ASM 

50050  126 
Finite_Reachable 
52394  127 
Denotational 
52400  128 
Compiler2 
48481  129 
Poly_Types 
130 
Sec_Typing 

131 
Sec_TypingT 

52726  132 
Def_Init_Big 
133 
Def_Init_Small 

134 
Fold 

48481  135 
Live 
136 
Live_True 

137 
Hoare_Examples 

52269  138 
VCG 
52282  139 
Hoare_Total 
48481  140 
Collecting1 
48765
fb1ed5230abc
special code with lists no longer necessary, use sets
nipkow
parents:
48738
diff
changeset

141 
Collecting_Examples 
48481  142 
Abs_Int_Tests 
143 
Abs_Int1_parity 

144 
Abs_Int1_const 

145 
Abs_Int3 

146 
"Abs_Int_ITP/Abs_Int1_parity_ITP" 

147 
"Abs_Int_ITP/Abs_Int1_const_ITP" 

148 
"Abs_Int_ITP/Abs_Int3_ITP" 

149 
"Abs_Int_Den/Abs_Int_den2" 

150 
Procs_Dyn_Vars_Dyn 

151 
Procs_Stat_Vars_Dyn 

152 
Procs_Stat_Vars_Stat 

153 
C_like 

154 
OO 

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

155 
document_files "root.bib" "root.tex" 
48481  156 

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

157 
session "HOLIMPP" in IMPP = HOL + 
48481  158 
description {* 
159 
Author: David von Oheimb 

160 
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

161 

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

162 
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

163 

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

164 
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

165 
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

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

168 
options [document = false] 
48481  169 
theories EvenOdd 
170 

61203  171 
session "HOLData_Structures" in Data_Structures = HOL + 
172 
options [document_variants = document] 

173 
theories [document = false] 

174 
"Less_False" 

175 
theories 

176 
Tree_Map 

61232  177 
AVL_Map 
61224  178 
RBT_Map 
61469
cd82b1023932
added 23 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
61368
diff
changeset

179 
Tree23_Map 
61514  180 
Tree234_Map 
61789  181 
Brother12_Map 
61525  182 
Splay_Map 
61224  183 
document_files "root.tex" "root.bib" 
61203  184 

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

185 
session "HOLImport" in Import = HOL + 
48481  186 
theories HOL_Light_Maps 
187 
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 

188 

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

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

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

191 
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

192 
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

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

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

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

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

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

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

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

200 
Pocklington 
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
55663
diff
changeset

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

202 
Number_Theory 
58023
62826b36ac5e
generic euclidean algorithm (due to Manuel Eberl)
haftmann
parents:
57998
diff
changeset

203 
Euclidean_Algorithm 
60804  204 
Factorial_Ring 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

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

206 
"root.tex" 
48481  207 

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

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

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

210 
Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

211 
Theorem, Wilson's Theorem, Quadratic Reciprocity. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

212 
*} 
48481  213 
theories [document = false] 
214 
"~~/src/HOL/Library/Infinite_Set" 

215 
"~~/src/HOL/Library/Permutation" 

216 
theories 

217 
Fib 

218 
Factorization 

219 
Chinese 

220 
WilsonRuss 

221 
WilsonBij 

222 
Quadratic_Reciprocity 

223 
Primes 

224 
Pocklington 

58623  225 
document_files 
226 
"root.bib" 

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 

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

237 
session "HOLHoare_Parallel" 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" + 
59992  246 
options [condition = ML_SYSTEM_POLYML, 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 
58415  253 
theories [condition = ISABELLE_GHC] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

254 
Code_Test_GHC 
58415  255 
theories [condition = ISABELLE_MLTON] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

256 
Code_Test_MLton 
58415  257 
theories [condition = ISABELLE_OCAMLC] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

258 
Code_Test_OCaml 
58415  259 
theories [condition = ISABELLE_POLYML] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

260 
Code_Test_PolyML 
58415  261 
theories [condition = ISABELLE_SCALA] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

262 
Code_Test_Scala 
58415  263 
theories [condition = ISABELLE_SMLNJ] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

264 
Code_Test_SMLNJ 
48481  265 

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

266 
session "HOLMetis_Examples" in Metis_Examples = HOL + 
48481  267 
description {* 
268 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

269 
Author: Jasmin Blanchette, TU Muenchen 

270 

271 
Testing Metis and Sledgehammer. 

272 
*} 

58423  273 
options [document = false] 
48481  274 
theories 
275 
Abstraction 

276 
Big_O 

277 
Binary_Tree 

278 
Clausification 

279 
Message 

280 
Proxies 

281 
Tarski 

282 
Trans_Closure 

283 
Sets 

284 

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

288 
Copyright 2009 

289 
*} 

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

290 
options [document = false] 
48481  291 
theories [quick_and_dirty] Nitpick_Examples 
292 

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

293 
session "HOLAlgebra" (main) in Algebra = HOL + 
48481  294 
description {* 
295 
Author: Clemens Ballarin, started 24 September 1999 

296 

297 
The Isabelle Algebraic Library. 

298 
*} 

299 
theories [document = false] 

300 
(* Preliminaries from set and number theory *) 

301 
"~~/src/HOL/Library/FuncSet" 

55159
608c157d743d
Replacing the theory Library/Binomial by Number_Theory/Binomial
paulson <lp15@cam.ac.uk>
parents:
55123
diff
changeset

302 
"~~/src/HOL/Number_Theory/Primes" 
48481  303 
"~~/src/HOL/Library/Permutation" 
304 
theories 

305 
(*** New development, based on explicit structures ***) 

306 
(* Groups *) 

307 
FiniteProduct (* Product operator for commutative groups *) 

308 
Sylow (* Sylow's theorem *) 

309 
Bij (* Automorphism Groups *) 

310 

311 
(* Rings *) 

312 
Divisibility (* Rings *) 

313 
IntRing (* Ideals and residue classes *) 

314 
UnivPoly (* Polynomials *) 

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

315 
document_files "root.bib" "root.tex" 
48481  316 

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

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

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

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

320 
*} 
48481  321 
theories 
322 
Auth_Shared 

323 
Auth_Public 

324 
"Smartcard/Auth_Smartcard" 

325 
"Guard/Auth_Guard_Shared" 

326 
"Guard/Auth_Guard_Public" 

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

327 
document_files "root.tex" 
48481  328 

51236
f301ad90c48b
more explicit session dependency, for improved parallel performance of HOLUNITY test session  NB: separate 'theories' sections are sequential;
wenzelm
parents:
51161
diff
changeset

329 
session "HOLUNITY" in UNITY = "HOLAuth" + 
48481  330 
description {* 
331 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

332 
Copyright 1998 University of Cambridge 

333 

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

334 
Verifying security protocols using Chandy and Misra's UNITY formalism. 
48481  335 
*} 
336 
theories 

337 
(*Basic metatheory*) 

338 
"UNITY_Main" 

339 

340 
(*Simple examples: no composition*) 

341 
"Simple/Deadlock" 

342 
"Simple/Common" 

343 
"Simple/Network" 

344 
"Simple/Token" 

345 
"Simple/Channel" 

346 
"Simple/Lift" 

347 
"Simple/Mutex" 

348 
"Simple/Reach" 

349 
"Simple/Reachability" 

350 

351 
(*Verifying security protocols using UNITY*) 

352 
"Simple/NSP_Bad" 

353 

354 
(*Example of composition*) 

355 
"Comp/Handshake" 

356 

357 
(*Universal properties examples*) 

358 
"Comp/Counter" 

359 
"Comp/Counterc" 

360 
"Comp/Priority" 

361 

362 
"Comp/TimerArray" 

363 
"Comp/Progress" 

364 

365 
"Comp/Alloc" 

366 
"Comp/AllocImpl" 

367 
"Comp/Client" 

368 

369 
(*obsolete*) 

370 
"ELT" 

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

371 
document_files "root.tex" 
48481  372 

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

373 
session "HOLUnix" in Unix = HOL + 
48481  374 
options [print_mode = "no_brackets,no_type_brackets"] 
375 
theories Unix 

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

376 
document_files "root.bib" "root.tex" 
48481  377 

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

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

380 
document_files "root.tex" 
48481  381 

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

382 
session "HOLImperative_HOL" in Imperative_HOL = HOL + 
59446  383 
options [print_mode = "iff,no_brackets"] 
48481  384 
theories [document = false] 
385 
"~~/src/HOL/Library/Countable" 

386 
"~~/src/HOL/Library/Monad_Syntax" 

387 
"~~/src/HOL/Library/LaTeXsugar" 

388 
theories Imperative_HOL_ex 

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

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

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

391 
session "HOLDecision_Procs" in Decision_Procs = HOL + 
51544  392 
description {* 
393 
Various decision procedures, typically involving reflection. 

394 
*} 

58413
22dd971f6938
renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
wenzelm
parents:
58385
diff
changeset

395 
options [condition = ML_SYSTEM_POLYML, document = false] 
48481  396 
theories Decision_Procs 
397 

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

398 
session "HOLProofsex" in "Proofs/ex" = "HOLProofs" + 
52499  399 
options [document = false, parallel_proofs = 0] 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
52400
diff
changeset

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

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

402 
XML_Data 
48481  403 

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

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

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

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

407 
*} 
59006
272d7fb92396
no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";
wenzelm
parents:
58849
diff
changeset

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

410 
"~~/src/HOL/Library/Code_Target_Numeral" 
48481  411 
"~~/src/HOL/Library/Monad_Syntax" 
412 
"~~/src/HOL/Number_Theory/Primes" 

413 
"~~/src/HOL/Number_Theory/UniqueFactorization" 

414 
"~~/src/HOL/Library/State_Monad" 

415 
theories 

416 
Greatest_Common_Divisor 

417 
Warshall 

418 
Higman_Extraction 

419 
Pigeonhole 

420 
Euclid 

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

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

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

423 
session "HOLProofsLambda" 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

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

425 
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

426 

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

427 
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

428 
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

429 

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

430 
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

431 
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

432 
*} 
59446  433 
options [print_mode = "no_brackets", parallel_proofs = 0, quick_and_dirty = false] 
48481  434 
theories [document = false] 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51115
diff
changeset

435 
"~~/src/HOL/Library/Code_Target_Int" 
48481  436 
theories 
437 
Eta 

438 
StrongNorm 

439 
Standardization 

440 
WeakNorm 

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

441 
document_files "root.bib" "root.tex" 
48481  442 

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

443 
session "HOLProlog" in Prolog = HOL + 
48481  444 
description {* 
445 
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

446 

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

447 
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

448 

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

449 
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

450 
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

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

453 
options [document = false] 
48481  454 
theories Test Type 
455 

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

456 
session "HOLMicroJava" 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

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

458 
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

459 
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

460 
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

461 
*} 
59446  462 
theories [document = false] 
463 
"~~/src/HOL/Library/While_Combinator" 

464 
theories 

465 
MicroJava 

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

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

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

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

469 
"root.tex" 
48481  470 

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

471 
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

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

473 
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

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

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

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

478 
session "HOLBali" in Bali = HOL + 
48481  479 
theories 
480 
AxExample 

481 
AxSound 

482 
AxCompl 

483 
Trans 

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

485 
document_files "root.tex" 
48481  486 

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

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

489 
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

490 
Copyright 19941996 TU Muenchen 
48481  491 

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

492 
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

493 
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

494 
proofs of two communication protocols which formerly have been here. 
48481  495 

496 
@inproceedings{NipkowSlindIOA, 

497 
author={Tobias Nipkow and Konrad Slind}, 

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

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

500 
publisher=Springer, 

501 
series=LNCS, 

502 
note={To appear}} 

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

504 

505 
and 

506 

507 
@inproceedings{MuellerNipkow, 

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

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

510 
booktitle={Proc.\ TACAS Workshop}, 

511 
organization={Aarhus University, BRICS report}, 

512 
year=1995} 

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

514 
*} 

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

515 
options [document = false] 
48481  516 
theories Solve 
517 

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

518 
session "HOLLattice" in Lattice = HOL + 
48481  519 
description {* 
520 
Author: Markus Wenzel, TU Muenchen 

521 

522 
Basic theory of lattices and orders. 

523 
*} 

524 
theories CompleteLattice 

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

525 
document_files "root.tex" 
48481  526 

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

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

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

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

530 
*} 
58423  531 
options [condition = ML_SYSTEM_POLYML] 
48481  532 
theories [document = false] 
533 
"~~/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

534 
Code_Binary_Nat_examples 
48481  535 
"~~/src/HOL/Library/FuncSet" 
536 
Eval_Examples 

537 
Normalization_by_Evaluation 

538 
Hebrew 

539 
Chinese 

540 
Serbian 

541 
"~~/src/HOL/Library/FinFun_Syntax" 

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

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

544 
Cartouche_Examples 
48481  545 
theories 
59090  546 
Commands 
57507  547 
Adhoc_Overloading_Examples 
48481  548 
Iff_Oracle 
549 
Coercion_Examples 

550 
Higher_Order_Logic 

551 
Abstract_NAT 

552 
Guess 

553 
Fundefs 

554 
Induction_Schema 

555 
LocaleTest2 

556 
Records 

557 
While_Combinator_Example 

558 
MonoidGroup 

559 
BinEx 

560 
Hex_Bin_Examples 

561 
Antiquote 

562 
Multiquote 

563 
PER 

564 
NatSum 

565 
ThreeDivides 

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

566 
Cubic_Quartic 
59739  567 
Pythagoras 
48481  568 
Intuitionistic 
569 
CTL 

570 
Arith_Examples 

571 
Tree23 

58644  572 
Bubblesort 
48481  573 
MergeSort 
574 
Lagrange 

575 
Groebner_Examples 

576 
MT 

577 
Unification 

578 
Primrec 

579 
Tarski 

580 
Classical 

581 
Set_Theory 

582 
Termination 

583 
Coherent 

584 
PresburgerEx 

51093  585 
Reflection_Examples 
48481  586 
Sqrt 
587 
Sqrt_Script 

61368  588 
Transfer_Debug 
48481  589 
Transfer_Ex 
590 
Transfer_Int_Nat 

56922  591 
Transitive_Closure_Table_Ex 
48481  592 
HarmonicSeries 
593 
Refute_Examples 

594 
Execute_Choice 

595 
Gauge_Integration 

596 
Dedekind_Real 

597 
Quicksort 

598 
Birthday_Paradox 

599 
List_to_Set_Comprehension_Examples 

600 
Seq 

601 
Simproc_Tests 

602 
Executable_Relation 

603 
FinFunPred 

55663  604 
Set_Comprehension_Pointfree_Examples 
48481  605 
Parallel_Example 
50138  606 
IArray_Examples 
53430  607 
Simps_Case_Conv_Examples 
53935  608 
ML 
59739  609 
Rewrite_Examples 
56815  610 
SAT_Examples 
58630  611 
SOS 
58418  612 
SOS_Cert 
60603
09ecbd791d4a
add examples from Freek's top 100 theorems (thms 30, 73, 77)
bulwahn
parents:
60470
diff
changeset

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

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

615 
Sum_of_Powers 
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

616 
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

617 
Meson_Test 
58331
054e9a9fccad
enabled 'Sudoku' only with 'ISABELLE_FULL_TEST'  Sudoku is fast enough on modern hardware (within seconds on my MacBook), but it seems to fail on older test machines
blanchet
parents:
58329
diff
changeset

618 
theories [condition = ISABELLE_FULL_TEST] 
054e9a9fccad
enabled 'Sudoku' only with 'ISABELLE_FULL_TEST'  Sudoku is fast enough on modern hardware (within seconds on my MacBook), but it seems to fail on older test machines
blanchet
parents:
58329
diff
changeset

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

620 
document_files "root.bib" "root.tex" 
48481  621 

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

622 
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

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

624 
Miscellaneous Isabelle/Isar examples for HigherOrder Logic. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

625 
*} 
48481  626 
theories [document = false] 
627 
"~~/src/HOL/Library/Lattice_Syntax" 

628 
"../Number_Theory/Primes" 

629 
theories 

630 
Basic_Logic 

631 
Cantor 

632 
Drinker 

633 
Expr_Compiler 

634 
Fibonacci 

635 
Group 

636 
Group_Context 

637 
Group_Notepad 

638 
Hoare_Ex 

639 
Knaster_Tarski 

640 
Mutilated_Checkerboard 

641 
Nested_Datatype 

642 
Peirce 

643 
Puzzle 

644 
Summation 

60470  645 
theories [quick_and_dirty] 
60450  646 
Structured_Statements 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

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

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

649 
"root.tex" 
48481  650 

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

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

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

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

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

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

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

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

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

659 

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

660 
session "HOLSET_Protocol" 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

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

662 
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

663 
*} 
48481  664 
theories [document = false] "~~/src/HOL/Library/Nat_Bijection" 
665 
theories SET_Protocol 

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

666 
document_files "root.tex" 
48481  667 

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

668 
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

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

670 
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

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

673 
document_files "root.tex" 
48481  674 

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

675 
session "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

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

677 
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

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

679 
options [document = false] 
48481  680 
theories TLA 
681 

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

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

683 
options [document = false] 
48481  684 
theories Inc 
685 

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

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

687 
options [document = false] 
48481  688 
theories DBuffer 
689 

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

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

691 
options [document = false] 
48481  692 
theories MemoryImplementation 
693 

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

694 
session "HOLTPTP" in TPTP = HOL + 
48481  695 
description {* 
696 
Author: Jasmin Blanchette, TU Muenchen 

697 
Author: Nik Sultana, University of Cambridge 

698 
Copyright 2011 

699 

700 
TPTPrelated extensions. 

701 
*} 

59992  702 
options [condition = ML_SYSTEM_POLYML, document = false] 
48481  703 
theories 
704 
ATP_Theory_Export 

705 
MaSh_Eval 

706 
TPTP_Interpret 

707 
THF_Arith 

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

708 
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

709 
theories 
48481  710 
ATP_Problem_Import 
711 

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

712 
session "HOLMultivariate_Analysis" (main) in Multivariate_Analysis = HOL + 
48481  713 
theories 
714 
Multivariate_Analysis 

715 
Determinants 

56215  716 
PolyRoots 
717 
Complex_Analysis_Basics 

59741
5b762cd73a8e
Lots of new material on complexvalued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

718 
Complex_Transcendental 
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60804
diff
changeset

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

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

721 
"root.tex" 
48481  722 

59922
1b6283aa7c94
rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
wenzelm
parents:
59903
diff
changeset

723 
session "HOLMultivariate_Analysisex" in "Multivariate_Analysis/ex" = "HOLMultivariate_Analysis" + 
1b6283aa7c94
rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
wenzelm
parents:
59903
diff
changeset

724 
theories 
1b6283aa7c94
rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
wenzelm
parents:
59903
diff
changeset

725 
Approximations 
1b6283aa7c94
rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
wenzelm
parents:
59903
diff
changeset

726 

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

727 
session "HOLProbability" in "Probability" = "HOLMultivariate_Analysis" + 
48481  728 
theories [document = false] 
729 
"~~/src/HOL/Library/Countable" 

730 
"~~/src/HOL/Library/Permutation" 

56994  731 
"~~/src/HOL/Library/Order_Continuity" 
732 
"~~/src/HOL/Library/Diagonal_Subsequence" 

48481  733 
theories 
734 
Probability 

735 
"ex/Dining_Cryptographers" 

736 
"ex/Koepf_Duermuth_Countermeasure" 

59144
c9b75c03de3c
unfortunately, there is no general function space in the measurable spaces
hoelzl
parents:
59090
diff
changeset

737 
"ex/Measure_Not_CCC" 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

738 
document_files "root.tex" 
48481  739 

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

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

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

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

744 
session "HOLNominalExamples" in "Nominal/Examples" = "HOLNominal" + 
58423  745 
options [condition = ML_SYSTEM_POLYML, document = false] 
58329
a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents:
58313
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

768 
VC_Condition 
48481  769 

55054
e1f3714bc508
moved subset of 'HOLCardinals' needed for BNF into 'HOL'
blanchet
parents:
55033
diff
changeset

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

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

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

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

774 
options [document = false] 
59747  775 
theories 
776 
Cardinals 

777 
Bounded_Set 

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

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

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

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

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

782 

58309
a09ec6daaa19
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
blanchet
parents:
58308
diff
changeset

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

784 
description {* 
58312  785 
(Co)datatype Examples, including large ones from John Harrison. 
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

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

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

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

789 
"~~/src/HOL/Library/Old_Datatype" 
56454  790 
Compat 
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset

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

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

793 
TreeFsetI 
49872  794 
"Derivation_Trees/Gram_Lang" 
795 
"Derivation_Trees/Parallel" 

50517  796 
Koenig 
60921  797 
Lift_BNF 
61745  798 
Milner_Tofte 
54961  799 
Stream_Processor 
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset

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

801 
Misc_Datatype 
54193  802 
Misc_Primcorec 
53306  803 
Misc_Primrec 
58849
ef7700ecce83
discontinued pointless option: timing is always on (overall theory only);
wenzelm
parents:
58842
diff
changeset

804 
theories [condition = ISABELLE_FULL_TEST] 
58308  805 
Brackin 
58313  806 
IsaFoR 
58433
d518f892cec6
made N2M tests conditional, since they appear to cause Isatest timeouts and are kind of slow
blanchet
parents:
58423
diff
changeset

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

808 

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

809 
session "HOLWord" (main) in Word = HOL + 
48481  810 
theories Word 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

811 
document_files "root.bib" "root.tex" 
48481  812 

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

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

814 
options [document = false] 
48481  815 
theories WordExamples 
816 

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

817 
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

818 
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

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

820 
document_files "root.tex" 
48481  821 

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

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

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

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

825 
*} 
48481  826 
theories Hypercomplex 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

827 
document_files "root.tex" 
48481  828 

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

829 
session "HOLNSAExamples" in "NSA/Examples" = "HOLNSA" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

830 
options [document = false] 
48481  831 
theories NSPrimes 
832 

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

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

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

836 

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

837 
session "HOLMirabelleex" in "Mirabelle/ex" = "HOLMirabelle" + 
60008  838 
options [condition = ML_SYSTEM_POLYML, 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

839 
theories Ex 
48481  840 

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

841 
session "HOLWordSMT_Examples" in SMT_Examples = "HOLWord" + 
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset

842 
options [document = false, quick_and_dirty] 
48481  843 
theories 
52722  844 
Boogie 
48481  845 
SMT_Examples 
846 
SMT_Word_Examples 

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

847 
theories [condition = ISABELLE_FULL_TEST] 
6f48853f08d5
actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
blanchet
parents:
50665
diff
changeset

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

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

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

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

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

854 
"VCC_Max.certs" 
48481  855 

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

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

857 
options [document = false] 
48481  858 
theories SPARK 
859 

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

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

861 
options [document = false, spark_prv = false] 
48481  862 
theories 
863 
"Gcd/Greatest_Common_Divisor" 

864 

865 
"Liseq/Longest_Increasing_Subsequence" 

866 

867 
"RIPEMD160/F" 

868 
"RIPEMD160/Hash" 

869 
"RIPEMD160/K_L" 

870 
"RIPEMD160/K_R" 

871 
"RIPEMD160/R_L" 

872 
"RIPEMD160/Round" 

873 
"RIPEMD160/R_R" 

874 
"RIPEMD160/S_L" 

875 
"RIPEMD160/S_R" 

876 

877 
"Sqrt/Sqrt" 

878 
files 

879 
"Gcd/greatest_common_divisor/g_c_d.fdl" 

880 
"Gcd/greatest_common_divisor/g_c_d.rls" 

881 
"Gcd/greatest_common_divisor/g_c_d.siv" 

882 
"Liseq/liseq/liseq_length.fdl" 

883 
"Liseq/liseq/liseq_length.rls" 

884 
"Liseq/liseq/liseq_length.siv" 

885 
"RIPEMD160/rmd/f.fdl" 

886 
"RIPEMD160/rmd/f.rls" 

887 
"RIPEMD160/rmd/f.siv" 

888 
"RIPEMD160/rmd/hash.fdl" 

889 
"RIPEMD160/rmd/hash.rls" 

890 
"RIPEMD160/rmd/hash.siv" 

891 
"RIPEMD160/rmd/k_l.fdl" 

892 
"RIPEMD160/rmd/k_l.rls" 

893 
"RIPEMD160/rmd/k_l.siv" 

894 
"RIPEMD160/rmd/k_r.fdl" 

895 
"RIPEMD160/rmd/k_r.rls" 

896 
"RIPEMD160/rmd/k_r.siv" 

897 
"RIPEMD160/rmd/r_l.fdl" 

898 
"RIPEMD160/rmd/r_l.rls" 

899 
"RIPEMD160/rmd/r_l.siv" 

900 
"RIPEMD160/rmd/round.fdl" 

901 
"RIPEMD160/rmd/round.rls" 

902 
"RIPEMD160/rmd/round.siv" 

903 
"RIPEMD160/rmd/r_r.fdl" 

904 
"RIPEMD160/rmd/r_r.rls" 

905 
"RIPEMD160/rmd/r_r.siv" 

906 
"RIPEMD160/rmd/s_l.fdl" 

907 
"RIPEMD160/rmd/s_l.rls" 

908 
"RIPEMD160/rmd/s_l.siv" 

909 
"RIPEMD160/rmd/s_r.fdl" 

910 
"RIPEMD160/rmd/s_r.rls" 

911 
"RIPEMD160/rmd/s_r.siv" 

912 

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

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

914 
options [show_question_marks = false, spark_prv = false] 
48481  915 
theories 
916 
Example_Verification 

917 
VC_Principles 

918 
Reference 

919 
Complex_Types 

920 
files 

921 
"complex_types_app/initialize.fdl" 

922 
"complex_types_app/initialize.rls" 

923 
"complex_types_app/initialize.siv" 

924 
"loop_invariant/proc1.fdl" 

925 
"loop_invariant/proc1.rls" 

926 
"loop_invariant/proc1.siv" 

927 
"loop_invariant/proc2.fdl" 

928 
"loop_invariant/proc2.rls" 

929 
"loop_invariant/proc2.siv" 

930 
"simple_greatest_common_divisor/g_c_d.fdl" 

931 
"simple_greatest_common_divisor/g_c_d.rls" 

932 
"simple_greatest_common_divisor/g_c_d.siv" 

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

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

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

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

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

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

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

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

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

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

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

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

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

945 
"Simple_Gcd.ads" 
48481  946 

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

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

948 
options [document = false] 
48481  949 
theories MutabelleExtra 
950 

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

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

952 
options [document = false] 
48588  953 
theories 
48690  954 
Quickcheck_Examples 
955 
Quickcheck_Lattice_Examples 

956 
Completeness 

957 
Quickcheck_Interfaces 

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

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

959 
Hotel_Example 
48598  960 
Quickcheck_Narrowing_Examples 
48588  961 

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

962 
session "HOLQuickcheck_Benchmark" in Quickcheck_Benchmark = HOL + 
50571
b649e33e4821
HOLQuickcheck_Benchmark works without timeout (NB: isatest imposes global timeout already);
wenzelm
parents:
50568
diff
changeset

963 
theories [condition = ISABELLE_FULL_TEST, quick_and_dirty] 
50568
ee090b5712f3
reverting d466ebc27810 as the previous changeset should allow to run Find_Unused_Assms_Examples again
bulwahn
parents:
50517
diff
changeset

964 
Find_Unused_Assms_Examples 
48618
1f7e068b4613
moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents:
48614
diff
changeset

965 
Needham_Schroeder_No_Attacker_Example 
1f7e068b4613
moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents:
48614
diff
changeset

966 
Needham_Schroeder_Guided_Attacker_Example 
48690  967 
Needham_Schroeder_Unguided_Attacker_Example 
48481  968 

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

969 
session "HOLQuotient_Examples" in Quotient_Examples = HOL + 
48481  970 
description {* 
971 
Author: Cezary Kaliszyk and Christian Urban 

972 
*} 

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

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

976 
FSet 

977 
Quotient_Int 

978 
Quotient_Message 

979 
Lift_FSet 

980 
Lift_Set 

981 
Lift_Fun 

982 
Quotient_Rat 

983 
Lift_DList 

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

984 
Int_Pow 
60237  985 
Lifting_Code_Dt_Test 
48481  986 

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

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

988 
options [document = false] 
48690  989 
theories 
48481  990 
Examples 
991 
Predicate_Compile_Tests 

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

992 
Predicate_Compile_Quickcheck_Examples 
48481  993 
Specialisation_Examples 
48690  994 
IMP_1 
995 
IMP_2 

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

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

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

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

1000 
theories [condition = "ISABELLE_SWIPL"] 
48690  1001 
Code_Prolog_Examples 
1002 
Context_Free_Grammar_Example 

1003 
Hotel_Example_Prolog 

1004 
Lambda_Example 

1005 
List_Examples 

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

1006 
theories [condition = "ISABELLE_SWIPL", quick_and_dirty] 
48690  1007 
Reg_Exp_Example 
48481  1008 

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

1009 
session HOLCF (main) in HOLCF = HOL + 
48338  1010 
description {* 
1011 
Author: Franz Regensburger 

1012 
Author: Brian Huffman 

1013 

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

1015 
*} 

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

1016 
theories [document = false] 
48338  1017 
"~~/src/HOL/Library/Nat_Bijection" 
1018 
"~~/src/HOL/Library/Countable" 

48481  1019 
theories 
1020 
Plain_HOLCF 

1021 
Fixrec 

1022 
HOLCF 

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

1023 
document_files "root.tex" 
48481  1024 

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

1025 
session "HOLCFTutorial" in "HOLCF/Tutorial" = HOLCF + 
48481  1026 
theories 
1027 
Domain_ex 

1028 
Fixrec_ex 

1029 
New_Domain 

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

1030 
document_files "root.tex" 
48481  1031 

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

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

1033 
options [document = false] 
48481  1034 
theories HOLCF_Library 
1035 

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

1036 
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

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

1038 
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

1039 

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

1040 
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

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

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

1044 
document_files "root.tex" 
48338  1045 

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

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

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

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

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

1050 
options [document = false] 
48481  1051 
theories 
1052 
Dnat 

1053 
Dagstuhl 

1054 
Focus_ex 

1055 
Fix2 

1056 
Hoare 

1057 
Concurrency_Monad 

1058 
Loop 

1059 
Powerdomain_ex 

1060 
Domain_Proofs 

1061 
Letrec 

1062 
Pattern_Match 

1063 

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

1064 
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

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

1066 
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

1067 

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

1068 
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

1069 

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

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

1071 
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

1072 

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

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

1074 
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

1075 

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

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

1077 
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

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

1079 
options [document = false] 
48481  1080 
theories 
1081 
Fstreams 

1082 
FOCUS 

1083 
Buffer_adm 

1084 

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

1085 
session IOA in "HOLCF/IOA" = HOLCF + 
48481  1086 
description {* 
1087 
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

1088 
Copyright 1997 TU München 
48481  1089 

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

1090 
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

1091 

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

1092 
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

1093 
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

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

1096 
options [document = false] 
48481  1097 
theories "meta_theory/Abstraction" 
1098 

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

1099 
session "IOAABP" in "HOLCF/IOA/ABP" = IOA + 
48481  1100 
description {* 
1101 
Author: Olaf Mueller 

1102 

1103 
The Alternating Bit Protocol performed in I/OAutomata. 

1104 
*} 

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

1105 
options [document = false] 
59503  1106 
theories 
1107 
Correctness 

1108 
Spec 

48481  1109 

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

1110 
session "IOANTP" in "HOLCF/IOA/NTP" = IOA + 
48481  1111 
description {* 
1112 
Author: Tobias Nipkow & Konrad Slind 

1113 

1114 
A network transmission protocol, performed in the 

1115 
I/O automata formalization by Olaf Mueller. 

1116 
*} 

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

1117 
options [document = false] 
48481  1118 
theories Correctness 
1119 

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

1120 
session "IOAStorage" in "HOLCF/IOA/Storage" = IOA + 
48481  1121 
description {* 
1122 
Author: Olaf Mueller 

1123 

1124 
Memory storage case study. 

1125 
*} 

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

1126 
options [document = false] 
48481  1127 
theories Correctness 
1128 

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

1129 
session "IOAex" in "HOLCF/IOA/ex" = IOA + 
48481  1130 
description {* 
1131 
Author: Olaf Mueller 

1132 
*} 

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

1133 
options [document = false] 
48481  1134 
theories 
1135 
TrivEx 

1136 
TrivEx2 

1137 

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

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

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

1140 
Some benchmark on large record. 
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset

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

1142 
options [document = false] 
58849
ef7700ecce83
discontinued pointless option: timing is always on (overall theory only);
wenzelm
parents:
58842
diff
changeset

1143 
theories [condition = ISABELLE_FULL_TEST] 
48481  1144 
Record_Benchmark 
1145 