author  paulson <lp15@cam.ac.uk> 
Tue, 28 Jul 2015 16:16:13 +0100  
changeset 60809  457abb82fb9e 
parent 60804  080a979a985b 
child 60921  487050067be9 
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 

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

17 
session "HOLProofs" = 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] 
55601  118 
"~~/src/Tools/Permanent_Interpretation" 
48481  119 
"~~/src/HOL/Library/While_Combinator" 
120 
"~~/src/HOL/Library/Char_ord" 

121 
"~~/src/HOL/Library/List_lexord" 

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

48481  124 
theories 
125 
BExp 

126 
ASM 

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

132 
Sec_TypingT 

52726  133 
Def_Init_Big 
134 
Def_Init_Small 

135 
Fold 

48481  136 
Live 
137 
Live_True 

138 
Hoare_Examples 

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

142 
Collecting_Examples 
48481  143 
Abs_Int_Tests 
144 
Abs_Int1_parity 

145 
Abs_Int1_const 

146 
Abs_Int3 

147 
"Abs_Int_ITP/Abs_Int1_parity_ITP" 

148 
"Abs_Int_ITP/Abs_Int1_const_ITP" 

149 
"Abs_Int_ITP/Abs_Int3_ITP" 

150 
"Abs_Int_Den/Abs_Int_den2" 

151 
Procs_Dyn_Vars_Dyn 

152 
Procs_Stat_Vars_Dyn 

153 
Procs_Stat_Vars_Stat 

154 
C_like 

155 
OO 

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

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

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

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

161 
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

162 

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

163 
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

164 

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

165 
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

166 
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

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

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

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

172 
session "HOLImport" in Import = HOL + 
48481  173 
theories HOL_Light_Maps 
174 
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 

175 

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

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

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

178 
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

179 
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

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

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

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

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

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

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

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

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

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

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

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

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

193 
"root.tex" 
48481  194 

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

195 
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

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

197 
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

198 
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

199 
*} 
48481  200 
theories [document = false] 
201 
"~~/src/HOL/Library/Infinite_Set" 

202 
"~~/src/HOL/Library/Permutation" 

203 
theories 

204 
Fib 

205 
Factorization 

206 
Chinese 

207 
WilsonRuss 

208 
WilsonBij 

209 
Quadratic_Reciprocity 

210 
Primes 

211 
Pocklington 

58623  212 
document_files 
213 
"root.bib" 

214 
"root.tex" 

48481  215 

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

216 
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

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

218 
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

219 
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

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

222 
document_files "root.bib" "root.tex" 
48481  223 

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

224 
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

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

226 
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

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

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

230 
document_files "root.bib" "root.tex" 
48481  231 

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

232 
session "HOLCodegenerator_Test" in Codegenerator_Test = "HOLLibrary" + 
59992  233 
options [condition = ML_SYSTEM_POLYML, document = false, browser_info = false] 
51422
821a70e29e0b
proper formatting, to facilitate linebased diff;
wenzelm
parents:
51421
diff
changeset

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

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

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

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

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

239 
Generate_Pretty_Char 
58415  240 
theories [condition = ISABELLE_GHC] 
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset

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

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

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

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

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

251 
Code_Test_SMLNJ 
48481  252 

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

253 
session "HOLMetis_Examples" in Metis_Examples = HOL + 
48481  254 
description {* 
255 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

256 
Author: Jasmin Blanchette, TU Muenchen 

257 

258 
Testing Metis and Sledgehammer. 

259 
*} 

58423  260 
options [document = false] 
48481  261 
theories 
262 
Abstraction 

263 
Big_O 

264 
Binary_Tree 

265 
Clausification 

266 
Message 

267 
Proxies 

268 
Tarski 

269 
Trans_Closure 

270 
Sets 

271 

55072  272 
session "HOLNitpick_Examples" in Nitpick_Examples = HOL + 
48481  273 
description {* 
274 
Author: Jasmin Blanchette, TU Muenchen 

275 
Copyright 2009 

276 
*} 

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

277 
options [document = false] 
48481  278 
theories [quick_and_dirty] Nitpick_Examples 
279 

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

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

283 

284 
The Isabelle Algebraic Library. 

285 
*} 

286 
theories [document = false] 

287 
(* Preliminaries from set and number theory *) 

288 
"~~/src/HOL/Library/FuncSet" 

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

289 
"~~/src/HOL/Number_Theory/Primes" 
48481  290 
"~~/src/HOL/Library/Permutation" 
291 
theories 

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

293 
(* Groups *) 

294 
FiniteProduct (* Product operator for commutative groups *) 

295 
Sylow (* Sylow's theorem *) 

296 
Bij (* Automorphism Groups *) 

297 

298 
(* Rings *) 

299 
Divisibility (* Rings *) 

300 
IntRing (* Ideals and residue classes *) 

301 
UnivPoly (* Polynomials *) 

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

302 
document_files "root.bib" "root.tex" 
48481  303 

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

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

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

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

307 
*} 
48481  308 
theories 
309 
Auth_Shared 

310 
Auth_Public 

311 
"Smartcard/Auth_Smartcard" 

312 
"Guard/Auth_Guard_Shared" 

313 
"Guard/Auth_Guard_Public" 

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

314 
document_files "root.tex" 
48481  315 

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

316 
session "HOLUNITY" in UNITY = "HOLAuth" + 
48481  317 
description {* 
318 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

319 
Copyright 1998 University of Cambridge 

320 

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

321 
Verifying security protocols using Chandy and Misra's UNITY formalism. 
48481  322 
*} 
323 
theories 

324 
(*Basic metatheory*) 

325 
"UNITY_Main" 

326 

327 
(*Simple examples: no composition*) 

328 
"Simple/Deadlock" 

329 
"Simple/Common" 

330 
"Simple/Network" 

331 
"Simple/Token" 

332 
"Simple/Channel" 

333 
"Simple/Lift" 

334 
"Simple/Mutex" 

335 
"Simple/Reach" 

336 
"Simple/Reachability" 

337 

338 
(*Verifying security protocols using UNITY*) 

339 
"Simple/NSP_Bad" 

340 

341 
(*Example of composition*) 

342 
"Comp/Handshake" 

343 

344 
(*Universal properties examples*) 

345 
"Comp/Counter" 

346 
"Comp/Counterc" 

347 
"Comp/Priority" 

348 

349 
"Comp/TimerArray" 

350 
"Comp/Progress" 

351 

352 
"Comp/Alloc" 

353 
"Comp/AllocImpl" 

354 
"Comp/Client" 

355 

356 
(*obsolete*) 

357 
"ELT" 

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

358 
document_files "root.tex" 
48481  359 

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

360 
session "HOLUnix" in Unix = HOL + 
48481  361 
options [print_mode = "no_brackets,no_type_brackets"] 
362 
theories Unix 

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

363 
document_files "root.bib" "root.tex" 
48481  364 

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

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

367 
document_files "root.tex" 
48481  368 

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

369 
session "HOLImperative_HOL" in Imperative_HOL = HOL + 
59446  370 
options [print_mode = "iff,no_brackets"] 
48481  371 
theories [document = false] 
372 
"~~/src/HOL/Library/Countable" 

373 
"~~/src/HOL/Library/Monad_Syntax" 

374 
"~~/src/HOL/Library/LaTeXsugar" 

375 
theories Imperative_HOL_ex 

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 "HOLDecision_Procs" in Decision_Procs = HOL + 
51544  379 
description {* 
380 
Various decision procedures, typically involving reflection. 

381 
*} 

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

382 
options [condition = ML_SYSTEM_POLYML, document = false] 
48481  383 
theories Decision_Procs 
384 

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

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

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

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

389 
XML_Data 
48481  390 

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

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

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

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

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

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

397 
"~~/src/HOL/Library/Code_Target_Numeral" 
48481  398 
"~~/src/HOL/Library/Monad_Syntax" 
399 
"~~/src/HOL/Number_Theory/Primes" 

400 
"~~/src/HOL/Number_Theory/UniqueFactorization" 

401 
"~~/src/HOL/Library/State_Monad" 

402 
theories 

403 
Greatest_Common_Divisor 

404 
Warshall 

405 
Higman_Extraction 

406 
Pigeonhole 

407 
Euclid 

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

408 
document_files "root.bib" "root.tex" 
48481  409 

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

410 
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

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

412 
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

413 

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

414 
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

415 
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

416 

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

417 
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

418 
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

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

422 
"~~/src/HOL/Library/Code_Target_Int" 
48481  423 
theories 
424 
Eta 

425 
StrongNorm 

426 
Standardization 

427 
WeakNorm 

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

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

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

430 
session "HOLProlog" in Prolog = HOL + 
48481  431 
description {* 
432 
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

433 

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

434 
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

435 

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

436 
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

437 
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

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

440 
options [document = false] 
48481  441 
theories Test Type 
442 

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

443 
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

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

445 
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

446 
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

447 
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

448 
*} 
59446  449 
theories [document = false] 
450 
"~~/src/HOL/Library/While_Combinator" 

451 
theories 

452 
MicroJava 

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

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

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

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

456 
"root.tex" 
48481  457 

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

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

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

460 
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

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

463 
document_files "root.bib" "root.tex" 
48481  464 

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

465 
session "HOLBali" in Bali = HOL + 
48481  466 
theories 
467 
AxExample 

468 
AxSound 

469 
AxCompl 

470 
Trans 

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

472 
document_files "root.tex" 
48481  473 

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

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

476 
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

477 
Copyright 19941996 TU Muenchen 
48481  478 

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

479 
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

480 
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

481 
proofs of two communication protocols which formerly have been here. 
48481  482 

483 
@inproceedings{NipkowSlindIOA, 

484 
author={Tobias Nipkow and Konrad Slind}, 

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

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

487 
publisher=Springer, 

488 
series=LNCS, 

489 
note={To appear}} 

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

491 

492 
and 

493 

494 
@inproceedings{MuellerNipkow, 

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

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

497 
booktitle={Proc.\ TACAS Workshop}, 

498 
organization={Aarhus University, BRICS report}, 

499 
year=1995} 

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

501 
*} 

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

502 
options [document = false] 
48481  503 
theories Solve 
504 

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

505 
session "HOLLattice" in Lattice = HOL + 
48481  506 
description {* 
507 
Author: Markus Wenzel, TU Muenchen 

508 

509 
Basic theory of lattices and orders. 

510 
*} 

511 
theories CompleteLattice 

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

512 
document_files "root.tex" 
48481  513 

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

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

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

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

517 
*} 
58423  518 
options [condition = ML_SYSTEM_POLYML] 
48481  519 
theories [document = false] 
520 
"~~/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

521 
Code_Binary_Nat_examples 
48481  522 
"~~/src/HOL/Library/FuncSet" 
523 
Eval_Examples 

524 
Normalization_by_Evaluation 

525 
Hebrew 

526 
Chinese 

527 
Serbian 

528 
"~~/src/HOL/Library/FinFun_Syntax" 

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

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

531 
Cartouche_Examples 
48481  532 
theories 
59090  533 
Commands 
57507  534 
Adhoc_Overloading_Examples 
48481  535 
Iff_Oracle 
536 
Coercion_Examples 

537 
Higher_Order_Logic 

538 
Abstract_NAT 

539 
Guess 

540 
Fundefs 

541 
Induction_Schema 

542 
LocaleTest2 

543 
Records 

544 
While_Combinator_Example 

545 
MonoidGroup 

546 
BinEx 

547 
Hex_Bin_Examples 

548 
Antiquote 

549 
Multiquote 

550 
PER 

551 
NatSum 

552 
ThreeDivides 

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

553 
Cubic_Quartic 
59739  554 
Pythagoras 
48481  555 
Intuitionistic 
556 
CTL 

557 
Arith_Examples 

558 
Tree23 

58644  559 
Bubblesort 
48481  560 
MergeSort 
561 
Lagrange 

562 
Groebner_Examples 

563 
MT 

564 
Unification 

565 
Primrec 

566 
Tarski 

567 
Classical 

568 
Set_Theory 

569 
Termination 

570 
Coherent 

571 
PresburgerEx 

51093  572 
Reflection_Examples 
48481  573 
Sqrt 
574 
Sqrt_Script 

575 
Transfer_Ex 

576 
Transfer_Int_Nat 

56922  577 
Transitive_Closure_Table_Ex 
48481  578 
HarmonicSeries 
579 
Refute_Examples 

580 
Execute_Choice 

581 
Gauge_Integration 

582 
Dedekind_Real 

583 
Quicksort 

584 
Birthday_Paradox 

585 
List_to_Set_Comprehension_Examples 

586 
Seq 

587 
Simproc_Tests 

588 
Executable_Relation 

589 
FinFunPred 

55663  590 
Set_Comprehension_Pointfree_Examples 
48481  591 
Parallel_Example 
50138  592 
IArray_Examples 
53430  593 
Simps_Case_Conv_Examples 
53935  594 
ML 
59739  595 
Rewrite_Examples 
56815  596 
SAT_Examples 
58630  597 
SOS 
58418  598 
SOS_Cert 
60603
09ecbd791d4a
add examples from Freek's top 100 theorems (thms 30, 73, 77)
bulwahn
parents:
60470
diff
changeset

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

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

601 
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

602 
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

603 
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

604 
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

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

606 
document_files "root.bib" "root.tex" 
48481  607 

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

608 
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

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

610 
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

611 
*} 
48481  612 
theories [document = false] 
613 
"~~/src/HOL/Library/Lattice_Syntax" 

614 
"../Number_Theory/Primes" 

615 
theories 

616 
Basic_Logic 

617 
Cantor 

618 
Drinker 

619 
Expr_Compiler 

620 
Fibonacci 

621 
Group 

622 
Group_Context 

623 
Group_Notepad 

624 
Hoare_Ex 

625 
Knaster_Tarski 

626 
Mutilated_Checkerboard 

627 
Nested_Datatype 

628 
Peirce 

629 
Puzzle 

630 
Summation 

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

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

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

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

636 
"style.tex" 
48481  637 

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

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

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

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

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

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

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

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

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

646 

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

647 
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

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

649 
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

650 
*} 
48481  651 
theories [document = false] "~~/src/HOL/Library/Nat_Bijection" 
652 
theories SET_Protocol 

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

653 
document_files "root.tex" 
48481  654 

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

655 
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

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

657 
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

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

660 
document_files "root.tex" 
48481  661 

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

662 
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

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

664 
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

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

666 
options [document = false] 
48481  667 
theories TLA 
668 

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

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

670 
options [document = false] 
48481  671 
theories Inc 
672 

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

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

674 
options [document = false] 
48481  675 
theories DBuffer 
676 

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

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

678 
options [document = false] 
48481  679 
theories MemoryImplementation 
680 

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

681 
session "HOLTPTP" in TPTP = HOL + 
48481  682 
description {* 
683 
Author: Jasmin Blanchette, TU Muenchen 

684 
Author: Nik Sultana, University of Cambridge 

685 
Copyright 2011 

686 

687 
TPTPrelated extensions. 

688 
*} 

59992  689 
options [condition = ML_SYSTEM_POLYML, document = false] 
48481  690 
theories 
691 
ATP_Theory_Export 

692 
MaSh_Eval 

693 
TPTP_Interpret 

694 
THF_Arith 

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

695 
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

696 
theories 
48481  697 
ATP_Problem_Import 
698 

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

699 
session "HOLMultivariate_Analysis" (main) in Multivariate_Analysis = HOL + 
48481  700 
theories 
701 
Multivariate_Analysis 

702 
Determinants 

56215  703 
PolyRoots 
704 
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

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

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

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

708 
"root.tex" 
48481  709 

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

710 
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

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

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

713 

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

714 
session "HOLProbability" in "Probability" = "HOLMultivariate_Analysis" + 
48481  715 
theories [document = false] 
716 
"~~/src/HOL/Library/Countable" 

717 
"~~/src/HOL/Library/Permutation" 

56994  718 
"~~/src/HOL/Library/Order_Continuity" 
719 
"~~/src/HOL/Library/Diagonal_Subsequence" 

48481  720 
theories 
721 
Probability 

722 
"ex/Dining_Cryptographers" 

723 
"ex/Koepf_Duermuth_Countermeasure" 

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

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

725 
document_files "root.tex" 
48481  726 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

755 
VC_Condition 
48481  756 

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

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

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

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

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

761 
options [document = false] 
59747  762 
theories 
763 
Cardinals 

764 
Bounded_Set 

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

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

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

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

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

769 

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

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

771 
description {* 
58312  772 
(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

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

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

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

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

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

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

780 
TreeFsetI 
49872  781 
"Derivation_Trees/Gram_Lang" 
782 
"Derivation_Trees/Parallel" 

50517  783 
Koenig 
54961  784 
Stream_Processor 
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset

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

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

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

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

793 

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

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

796 
document_files "root.bib" "root.tex" 
48481  797 

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

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

799 
options [document = false] 
48481  800 
theories WordExamples 
801 

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

802 
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

803 
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

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

805 
document_files "root.tex" 
48481  806 

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

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

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

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

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

812 
document_files "root.tex" 
48481  813 

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

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

815 
options [document = false] 
48481  816 
theories NSPrimes 
817 

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

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

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

821 

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

822 
session "HOLMirabelleex" in "Mirabelle/ex" = "HOLMirabelle" + 
60008  823 
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

824 
theories Ex 
48481  825 

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

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

827 
options [document = false, quick_and_dirty] 
48481  828 
theories 
52722  829 
Boogie 
48481  830 
SMT_Examples 
831 
SMT_Word_Examples 

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

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

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

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

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

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

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

839 
"VCC_Max.certs" 
48481  840 

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

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

842 
options [document = false] 
48481  843 
theories SPARK 
844 

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

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

846 
options [document = false, spark_prv = false] 
48481  847 
theories 
848 
"Gcd/Greatest_Common_Divisor" 

849 

850 
"Liseq/Longest_Increasing_Subsequence" 

851 

852 
"RIPEMD160/F" 

853 
"RIPEMD160/Hash" 

854 
"RIPEMD160/K_L" 

855 
"RIPEMD160/K_R" 

856 
"RIPEMD160/R_L" 

857 
"RIPEMD160/Round" 

858 
"RIPEMD160/R_R" 

859 
"RIPEMD160/S_L" 

860 
"RIPEMD160/S_R" 

861 

862 
"Sqrt/Sqrt" 

863 
files 

864 
"Gcd/greatest_common_divisor/g_c_d.fdl" 

865 
"Gcd/greatest_common_divisor/g_c_d.rls" 

866 
"Gcd/greatest_common_divisor/g_c_d.siv" 

867 
"Liseq/liseq/liseq_length.fdl" 

868 
"Liseq/liseq/liseq_length.rls" 

869 
"Liseq/liseq/liseq_length.siv" 

870 
"RIPEMD160/rmd/f.fdl" 

871 
"RIPEMD160/rmd/f.rls" 

872 
"RIPEMD160/rmd/f.siv" 

873 
"RIPEMD160/rmd/hash.fdl" 

874 
"RIPEMD160/rmd/hash.rls" 

875 
"RIPEMD160/rmd/hash.siv" 

876 
"RIPEMD160/rmd/k_l.fdl" 

877 
"RIPEMD160/rmd/k_l.rls" 

878 
"RIPEMD160/rmd/k_l.siv" 

879 
"RIPEMD160/rmd/k_r.fdl" 

880 
"RIPEMD160/rmd/k_r.rls" 

881 
"RIPEMD160/rmd/k_r.siv" 

882 
"RIPEMD160/rmd/r_l.fdl" 

883 
"RIPEMD160/rmd/r_l.rls" 

884 
"RIPEMD160/rmd/r_l.siv" 

885 
"RIPEMD160/rmd/round.fdl" 

886 
"RIPEMD160/rmd/round.rls" 

887 
"RIPEMD160/rmd/round.siv" 

888 
"RIPEMD160/rmd/r_r.fdl" 

889 
"RIPEMD160/rmd/r_r.rls" 

890 
"RIPEMD160/rmd/r_r.siv" 

891 
"RIPEMD160/rmd/s_l.fdl" 

892 
"RIPEMD160/rmd/s_l.rls" 

893 
"RIPEMD160/rmd/s_l.siv" 

894 
"RIPEMD160/rmd/s_r.fdl" 

895 
"RIPEMD160/rmd/s_r.rls" 

896 
"RIPEMD160/rmd/s_r.siv" 

897 

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

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

899 
options [show_question_marks = false, spark_prv = false] 
48481  900 
theories 
901 
Example_Verification 

902 
VC_Principles 

903 
Reference 

904 
Complex_Types 

905 
files 

906 
"complex_types_app/initialize.fdl" 

907 
"complex_types_app/initialize.rls" 

908 
"complex_types_app/initialize.siv" 

909 
"loop_invariant/proc1.fdl" 

910 
"loop_invariant/proc1.rls" 

911 
"loop_invariant/proc1.siv" 

912 
"loop_invariant/proc2.fdl" 

913 
"loop_invariant/proc2.rls" 

914 
"loop_invariant/proc2.siv" 

915 
"simple_greatest_common_divisor/g_c_d.fdl" 

916 
"simple_greatest_common_divisor/g_c_d.rls" 

917 
"simple_greatest_common_divisor/g_c_d.siv" 

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

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

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

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

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

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

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

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

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

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

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

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

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

930 
"Simple_Gcd.ads" 
48481  931 

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

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

933 
options [document = false] 
48481  934 
theories MutabelleExtra 
935 

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

936 
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

937 
options [document = false] 
48588  938 
theories 
48690  939 
Quickcheck_Examples 
940 
Quickcheck_Lattice_Examples 

941 
Completeness 

942 
Quickcheck_Interfaces 

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

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

944 
Hotel_Example 
48598  945 
Quickcheck_Narrowing_Examples 
48588  946 

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

947 
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

948 
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

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

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

951 
Needham_Schroeder_Guided_Attacker_Example 
48690  952 
Needham_Schroeder_Unguided_Attacker_Example 
48481  953 

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

954 
session "HOLQuotient_Examples" in Quotient_Examples = HOL + 
48481  955 
description {* 
956 
Author: Cezary Kaliszyk and Christian Urban 

957 
*} 

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

958 
options [document = false] 
48481  959 
theories 
960 
DList 

961 
FSet 

962 
Quotient_Int 

963 
Quotient_Message 

964 
Lift_FSet 

965 
Lift_Set 

966 
Lift_Fun 

967 
Quotient_Rat 

968 
Lift_DList 

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

969 
Int_Pow 
60237  970 
Lifting_Code_Dt_Test 
48481  971 

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

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

973 
options [document = false] 
48690  974 
theories 
48481  975 
Examples 
976 
Predicate_Compile_Tests 

48690  977 
(* FIXME 
978 
Predicate_Compile_Quickcheck_Examples  should be added again soon (since 21Oct2010) *) 

48481  979 
Specialisation_Examples 
48690  980 
IMP_1 
981 
IMP_2 

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

982 
(* FIXME since 21Jul2011 
9eddc17749f7
reactivate some examples that still appear to work;
wenzelm
parents:
55447
diff
changeset

983 
Hotel_Example_Small_Generator 
48690  984 
IMP_3 
985 
IMP_4 *) 

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

986 
theories [condition = "ISABELLE_SWIPL"] 
48690  987 
Code_Prolog_Examples 
988 
Context_Free_Grammar_Example 

989 
Hotel_Example_Prolog 

990 
Lambda_Example 

991 
List_Examples 

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

992 
theories [condition = "ISABELLE_SWIPL", quick_and_dirty] 
48690  993 
Reg_Exp_Example 
48481  994 

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

995 
session HOLCF (main) in HOLCF = HOL + 
48338  996 
description {* 
997 
Author: Franz Regensburger 

998 
Author: Brian Huffman 

999 

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

1001 
*} 

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

1002 
theories [document = false] 
48338  1003 
"~~/src/HOL/Library/Nat_Bijection" 
1004 
"~~/src/HOL/Library/Countable" 

48481  1005 
theories 
1006 
Plain_HOLCF 

1007 
Fixrec 

1008 
HOLCF 

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

1009 
document_files "root.tex" 
48481  1010 

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

1011 
session "HOLCFTutorial" in "HOLCF/Tutorial" = HOLCF + 
48481  1012 
theories 
1013 
Domain_ex 

1014 
Fixrec_ex 

1015 
New_Domain 

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

1016 
document_files "root.tex" 
48481  1017 

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

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

1019 
options [document = false] 
48481  1020 
theories HOLCF_Library 
1021 

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

1022 
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

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

1024 
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

1025 

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

1026 
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

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

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

1030 
document_files "root.tex" 
48338  1031 

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

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

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

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

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

1036 
options [document = false] 
48481  1037 
theories 
1038 
Dnat 

1039 
Dagstuhl 

1040 
Focus_ex 

1041 
Fix2 

1042 
Hoare 

1043 
Concurrency_Monad 

1044 
Loop 

1045 
Powerdomain_ex 

1046 
Domain_Proofs 

1047 
Letrec 

1048 
Pattern_Match 

1049 

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

1050 
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

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

1052 
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

1053 

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

1054 
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

1055 

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

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

1057 
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

1058 

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

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

1060 
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

1061 

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

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

1063 
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

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

1065 
options [document = false] 
48481  1066 
theories 
1067 
Fstreams 

1068 
FOCUS 

1069 
Buffer_adm 

1070 

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

1071 
session IOA in "HOLCF/IOA" = HOLCF + 
48481  1072 
description {* 
1073 
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

1074 
Copyright 1997 TU München 
48481  1075 

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

1076 
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

1077 

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

1078 
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

1079 
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

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

1082 
options [document = false] 
48481  1083 
theories "meta_theory/Abstraction" 
1084 

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

1085 
session "IOAABP" in "HOLCF/IOA/ABP" = IOA + 
48481  1086 
description {* 
1087 
Author: Olaf Mueller 

1088 

1089 
The Alternating Bit Protocol performed in I/OAutomata. 

1090 
*} 

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

1091 
options [document = false] 
59503  1092 
theories 
1093 
Correctness 

1094 
Spec 

48481  1095 

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

1096 
session "IOANTP" in "HOLCF/IOA/NTP" = IOA + 
48481  1097 
description {* 
1098 
Author: Tobias Nipkow & Konrad Slind 

1099 

1100 
A network transmission protocol, performed in the 

1101 
I/O automata formalization by Olaf Mueller. 

1102 
*} 

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

1103 
options [document = false] 
48481  1104 
theories Correctness 
1105 

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

1106 
session "IOAStorage" in "HOLCF/IOA/Storage" = IOA + 
48481  1107 
description {* 
1108 
Author: Olaf Mueller 

1109 

1110 
Memory storage case study. 

1111 
*} 

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

1112 
options [document = false] 
48481  1113 
theories Correctness 
1114 

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

1115 
session "IOAex" in "HOLCF/IOA/ex" = IOA + 
48481  1116 
description {* 
1117 
Author: Olaf Mueller 

1118 
*} 

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

1119 
options [document = false] 
48481  1120 
theories 
1121 
TrivEx 

1122 
TrivEx2 

1123 

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

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

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

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

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

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

1129 
theories [condition = ISABELLE_FULL_TEST] 
48481  1130 
Record_Benchmark 
1131 