author  wenzelm 
Wed, 14 Dec 2016 18:37:54 +0100  
changeset 64569  deebf3ff50e6 
parent 64555  628b271c5b8b 
child 64582  3d20ded18f14 
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 

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

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

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

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

20 
*} 
64569  21 
options [document = false, quick_and_dirty = false, parallel_proofs = 0] 
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!*) 
64569  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 

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

28 
session "HOLLibrary" (main timing) 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 

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

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

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

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

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

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

40 
(*conflicting type class instantiations*) 
48481  41 
List_lexord 
42 
Sublist_Order 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

64 
session "HOLHahn_Banach" in Hahn_Banach = HOL + 
48481  65 
description {* 
66 
Author: Gertrud Bauer, TU Munich 

67 

68 
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

69 

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

70 
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

71 
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

72 
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

73 
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

74 

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

75 
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

76 
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

77 

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

78 
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

79 
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

80 
continous linearform on the whole vectorspace. 
48481  81 
*} 
82 
theories Hahn_Banach 

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

83 
document_files "root.bib" "root.tex" 
48481  84 

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

85 
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

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

87 
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

88 

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

89 
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

90 
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

91 

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

92 
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

93 
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

94 

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

95 
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

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

97 
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

98 

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

99 
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

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

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

102 
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

103 
"~~/src/HOL/Library/Old_Datatype" 
48481  104 
theories [quick_and_dirty] 
105 
Common_Patterns 

106 
theories 

61935  107 
Nested_Datatype 
48481  108 
QuoDataType 
109 
QuoNestedDataType 

110 
Term 

111 
SList 

112 
ABexp 

113 
Tree 

114 
Ordinals 

115 
Sigma_Algebra 

116 
Comb 

117 
PropLog 

118 
Com 

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

119 
document_files "root.tex" 
48481  120 

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

121 
session "HOLIMP" (timing) in IMP = HOL + 
59446  122 
options [document_variants = document] 
48481  123 
theories [document = false] 
124 
"~~/src/HOL/Library/While_Combinator" 

125 
"~~/src/HOL/Library/Char_ord" 

126 
"~~/src/HOL/Library/List_lexord" 

51625  127 
"~~/src/HOL/Library/Quotient_List" 
128 
"~~/src/HOL/Library/Extended" 

48481  129 
theories 
130 
BExp 

131 
ASM 

50050  132 
Finite_Reachable 
52394  133 
Denotational 
52400  134 
Compiler2 
48481  135 
Poly_Types 
136 
Sec_Typing 

137 
Sec_TypingT 

52726  138 
Def_Init_Big 
139 
Def_Init_Small 

140 
Fold 

48481  141 
Live 
142 
Live_True 

143 
Hoare_Examples 

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

144 
Hoare_Sound_Complete 
52269  145 
VCG 
52282  146 
Hoare_Total 
63538
d7b5e2a222c2
added new vcg based on existentially quantified whilerule
nipkow
parents:
63537
diff
changeset

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

149 
Collecting_Examples 
48481  150 
Abs_Int_Tests 
151 
Abs_Int1_parity 

152 
Abs_Int1_const 

153 
Abs_Int3 

154 
Procs_Dyn_Vars_Dyn 

155 
Procs_Stat_Vars_Dyn 

156 
Procs_Stat_Vars_Stat 

157 
C_like 

158 
OO 

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

159 
document_files "root.bib" "root.tex" 
48481  160 

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

161 
session "HOLIMPP" in IMPP = HOL + 
48481  162 
description {* 
163 
Author: David von Oheimb 

164 
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

165 

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

166 
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

167 

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

168 
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

169 
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

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

172 
options [document = false] 
48481  173 
theories EvenOdd 
174 

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

175 
session "HOLData_Structures" (timing) in Data_Structures = HOL + 
61203  176 
options [document_variants = document] 
177 
theories [document = false] 

178 
"Less_False" 

62706  179 
"~~/src/HOL/Library/Multiset" 
64323  180 
"~~/src/HOL/Number_Theory/Fib" 
61203  181 
theories 
63829  182 
Balance 
61203  183 
Tree_Map 
61232  184 
AVL_Map 
61224  185 
RBT_Map 
61469
cd82b1023932
added 23 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
61368
diff
changeset

186 
Tree23_Map 
61514  187 
Tree234_Map 
61789  188 
Brother12_Map 
62130  189 
AA_Map 
61525  190 
Splay_Map 
62706  191 
Leftist_Heap 
61224  192 
document_files "root.tex" "root.bib" 
61203  193 

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

194 
session "HOLImport" in Import = HOL + 
48481  195 
theories HOL_Light_Maps 
196 
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 

197 

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

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

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

200 
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

201 
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

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

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

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

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

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

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

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

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

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

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

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

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

215 
"root.tex" 
48481  216 

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

217 
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

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

219 
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

220 
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

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

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

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

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

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

227 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

252 
Code_Test_SMLNJ 
48481  253 

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

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

257 
Author: Jasmin Blanchette, TU Muenchen 

258 

259 
Testing Metis and Sledgehammer. 

260 
*} 

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

264 
Big_O 

265 
Binary_Tree 

266 
Clausification 

267 
Message 

268 
Proxies 

269 
Tarski 

270 
Trans_Closure 

271 
Sets 

272 

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

276 
Copyright 2009 

277 
*} 

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

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

64389  281 
session "HOLNunchaku" in Nunchaku = HOL + 
282 
description {* 

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

284 
Copyright 2015, 2016 

285 

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

287 
*} 

288 
options [document = false] 

289 
theories Nunchaku 

290 

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

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

294 

295 
The Isabelle Algebraic Library. 

296 
*} 

297 
theories [document = false] 

298 
(* Preliminaries from set and number theory *) 

299 
"~~/src/HOL/Library/FuncSet" 

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

300 
"~~/src/HOL/Number_Theory/Primes" 
48481  301 
"~~/src/HOL/Library/Permutation" 
302 
theories 

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

304 
(* Groups *) 

305 
FiniteProduct (* Product operator for commutative groups *) 

306 
Sylow (* Sylow's theorem *) 

307 
Bij (* Automorphism Groups *) 

308 

309 
(* Rings *) 

310 
Divisibility (* Rings *) 

311 
IntRing (* Ideals and residue classes *) 

312 
UnivPoly (* Polynomials *) 

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

313 
document_files "root.bib" "root.tex" 
48481  314 

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

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

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

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

318 
*} 
48481  319 
theories 
320 
Auth_Shared 

321 
Auth_Public 

322 
"Smartcard/Auth_Smartcard" 

323 
"Guard/Auth_Guard_Shared" 

324 
"Guard/Auth_Guard_Public" 

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

325 
document_files "root.tex" 
48481  326 

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

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

330 
Copyright 1998 University of Cambridge 

331 

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

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

335 
(*Basic metatheory*) 

336 
"UNITY_Main" 

337 

338 
(*Simple examples: no composition*) 

339 
"Simple/Deadlock" 

340 
"Simple/Common" 

341 
"Simple/Network" 

342 
"Simple/Token" 

343 
"Simple/Channel" 

344 
"Simple/Lift" 

345 
"Simple/Mutex" 

346 
"Simple/Reach" 

347 
"Simple/Reachability" 

348 

349 
(*Verifying security protocols using UNITY*) 

350 
"Simple/NSP_Bad" 

351 

352 
(*Example of composition*) 

353 
"Comp/Handshake" 

354 

355 
(*Universal properties examples*) 

356 
"Comp/Counter" 

357 
"Comp/Counterc" 

358 
"Comp/Priority" 

359 

360 
"Comp/TimerArray" 

361 
"Comp/Progress" 

362 

363 
"Comp/Alloc" 

364 
"Comp/AllocImpl" 

365 
"Comp/Client" 

366 

367 
(*obsolete*) 

368 
"ELT" 

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

369 
document_files "root.tex" 
48481  370 

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

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

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

374 
document_files "root.bib" "root.tex" 
48481  375 

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

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

378 
document_files "root.tex" 
48481  379 

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

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

384 
"~~/src/HOL/Library/Monad_Syntax" 

385 
"~~/src/HOL/Library/LaTeXsugar" 

386 
theories Imperative_HOL_ex 

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

387 
document_files "root.bib" "root.tex" 
48481  388 

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

389 
session "HOLDecision_Procs" (timing) in Decision_Procs = HOL + 
51544  390 
description {* 
391 
Various decision procedures, typically involving reflection. 

392 
*} 

62354  393 
options [document = false] 
48481  394 
theories Decision_Procs 
395 

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

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

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

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

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

401 
XML_Data 
48481  402 

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

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

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

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

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

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

412 
"~~/src/HOL/Library/State_Monad" 

413 
theories 

414 
Greatest_Common_Divisor 

415 
Warshall 

416 
Higman_Extraction 

417 
Pigeonhole 

418 
Euclid 

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

419 
document_files "root.bib" "root.tex" 
48481  420 

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

421 
session "HOLProofsLambda" (timing) in "Proofs/Lambda" = "HOLProofs" + 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

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

423 
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

424 

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

425 
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

426 
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

427 

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

428 
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

429 
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

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

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

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

437 
StrongNorm 

438 
Standardization 

439 
WeakNorm 

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

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

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

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

445 

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

446 
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

447 

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

448 
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

449 
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

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

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

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

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

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

457 
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

458 
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

459 
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

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

463 
theories 

464 
MicroJava 

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

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

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

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

468 
"root.tex" 
48481  469 

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

470 
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

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

472 
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

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

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

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

477 
session "HOLBali" (timing) in Bali = HOL + 
48481  478 
theories 
479 
AxExample 

480 
AxSound 

481 
AxCompl 

482 
Trans 

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

484 
document_files "root.tex" 
48481  485 

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

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

488 
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

489 
Copyright 19941996 TU Muenchen 
48481  490 

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

491 
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

492 
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

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

495 
@inproceedings{NipkowSlindIOA, 

496 
author={Tobias Nipkow and Konrad Slind}, 

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

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

499 
publisher=Springer, 

500 
series=LNCS, 

501 
note={To appear}} 

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

503 

504 
and 

505 

506 
@inproceedings{MuellerNipkow, 

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

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

509 
booktitle={Proc.\ TACAS Workshop}, 

510 
organization={Aarhus University, BRICS report}, 

511 
year=1995} 

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

513 
*} 

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

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

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

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

520 

521 
Basic theory of lattices and orders. 

522 
*} 

523 
theories CompleteLattice 

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

524 
document_files "root.tex" 
48481  525 

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

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

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

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

529 
*} 
48481  530 
theories [document = false] 
531 
"~~/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

532 
Code_Binary_Nat_examples 
48481  533 
"~~/src/HOL/Library/FuncSet" 
534 
Eval_Examples 

535 
Normalization_by_Evaluation 

536 
Hebrew 

537 
Chinese 

538 
Serbian 

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

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

541 
Cartouche_Examples 
48481  542 
theories 
59090  543 
Commands 
57507  544 
Adhoc_Overloading_Examples 
48481  545 
Iff_Oracle 
546 
Coercion_Examples 

547 
Abstract_NAT 

548 
Guess 

62999  549 
Functions 
48481  550 
Induction_Schema 
551 
LocaleTest2 

552 
Records 

553 
While_Combinator_Example 

554 
MonoidGroup 

555 
BinEx 

556 
Hex_Bin_Examples 

557 
Antiquote 

558 
Multiquote 

559 
PER 

560 
NatSum 

561 
ThreeDivides 

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

562 
Cubic_Quartic 
59739  563 
Pythagoras 
48481  564 
Intuitionistic 
565 
CTL 

566 
Arith_Examples 

567 
Tree23 

58644  568 
Bubblesort 
48481  569 
MergeSort 
570 
Lagrange 

571 
Groebner_Examples 

572 
Unification 

573 
Primrec 

574 
Tarski 

575 
Classical 

576 
Set_Theory 

577 
Termination 

578 
Coherent 

579 
PresburgerEx 

51093  580 
Reflection_Examples 
48481  581 
Sqrt 
582 
Sqrt_Script 

61368  583 
Transfer_Debug 
48481  584 
Transfer_Ex 
585 
Transfer_Int_Nat 

56922  586 
Transitive_Closure_Table_Ex 
48481  587 
HarmonicSeries 
588 
Refute_Examples 

589 
Execute_Choice 

590 
Gauge_Integration 

591 
Dedekind_Real 

592 
Quicksort 

593 
Birthday_Paradox 

594 
List_to_Set_Comprehension_Examples 

595 
Seq 

596 
Simproc_Tests 

597 
Executable_Relation 

598 
FinFunPred 

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

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

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

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

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

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

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

615 
Word_Type 
51558
91f8bed6d0a4
allow build with skip_proofs enabled  disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents:
51553
diff
changeset

616 
theories [skip_proofs = false] 
91f8bed6d0a4
allow build with skip_proofs enabled  disable it for sessions that would fail due to embedded diagnostic commands, for example;
wenzelm
parents:
51553
diff
changeset

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

618 
document_files "root.bib" "root.tex" 
48481  619 

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

620 
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

621 
description {* 
61935  622 
Miscellaneous Isabelle/Isar examples. 
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

623 
*} 
61939  624 
options [quick_and_dirty] 
48481  625 
theories [document = false] 
626 
"~~/src/HOL/Library/Lattice_Syntax" 

627 
"../Number_Theory/Primes" 

628 
theories 

61939  629 
Knaster_Tarski 
630 
Peirce 

631 
Drinker 

48481  632 
Cantor 
61939  633 
Structured_Statements 
634 
Basic_Logic 

48481  635 
Expr_Compiler 
636 
Fibonacci 

637 
Group 

638 
Group_Context 

639 
Group_Notepad 

640 
Hoare_Ex 

641 
Mutilated_Checkerboard 

642 
Puzzle 

643 
Summation 

61935  644 
First_Order_Logic 
645 
Higher_Order_Logic 

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

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

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

648 
"root.tex" 
48481  649 

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

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

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

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

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

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

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

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

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

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

659 

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

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

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

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

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

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

666 
document_files "root.tex" 
48481  667 

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

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

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

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

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

673 
document_files "root.tex" 
48481  674 

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

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

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

677 
Lamport's Temporal Logic of Actions. 
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

697 
Author: Nik Sultana, University of Cambridge 

698 
Copyright 2011 

699 

700 
TPTPrelated extensions. 

701 
*} 

62354  702 
options [document = false] 
48481  703 
theories 
704 
ATP_Theory_Export 

705 
MaSh_Eval 

706 
TPTP_Interpret 

707 
THF_Arith 

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

708 
TPTP_Proof_Reconstruction 
52488
cd65ee49a8ba
discontinued system option "proofs"  global state of Proofterm.proofs is persistently compiled into HOLProofs image;
wenzelm
parents:
52424
diff
changeset

709 
theories 
48481  710 
ATP_Problem_Import 
711 

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

712 
session "HOLAnalysis" (main timing) in Analysis = HOL + 
48481  713 
theories 
63627  714 
Analysis 
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset

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

716 
"root.tex" 
48481  717 

63627  718 
session "HOLAnalysisex" in "Analysis/ex" = "HOLAnalysis" + 
59922
1b6283aa7c94
rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
wenzelm
parents:
59903
diff
changeset

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

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

721 

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

722 
session "HOLProbability" (timing) in "Probability" = "HOLAnalysis" + 
48481  723 
theories [document = false] 
724 
"~~/src/HOL/Library/Countable" 

725 
"~~/src/HOL/Library/Permutation" 

56994  726 
"~~/src/HOL/Library/Order_Continuity" 
727 
"~~/src/HOL/Library/Diagonal_Subsequence" 

63885
a6cd18af8bf9
new type for finite maps; use it in HOLProbability
Lars Hupel <lars.hupel@mytum.de>
parents:
63829
diff
changeset

728 
"~~/src/HOL/Library/Finite_Map" 
48481  729 
theories 
730 
Probability 

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

731 
document_files "root.tex" 
48481  732 

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

733 
session "HOLProbabilityex" (timing) in "Probability/ex" = "HOLProbability" + 
61946
844881193616
put example into separate session, to restrict precious session image to library theories
haftmann
parents:
61939
diff
changeset

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

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

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

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

738 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

767 
VC_Condition 
48481  768 

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

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

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

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

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

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

776 
Bounded_Set 

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

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

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

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

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

781 

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

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

783 
description {* 
62286
705d4c4003ea
clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build a" by default;
wenzelm
parents:
62285
diff
changeset

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

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

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

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

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

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

791 
TreeFsetI 
49872  792 
"Derivation_Trees/Gram_Lang" 
793 
"Derivation_Trees/Parallel" 

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

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

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

802 

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

803 
session "HOLCorec_Examples" (timing) in Corec_Examples = HOL + 
62694  804 
description {* 
805 
Corecursion Examples. 

806 
*} 

807 
options [document = false] 

808 
theories 

809 
LFilter 

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

813 
"Tests/Iterate_GPV" 
62696  814 
theories [quick_and_dirty] 
815 
"Tests/GPV_Bare_Bones" 

816 
"Tests/Merge_D" 

817 
"Tests/Merge_Poly" 

818 
"Tests/Misc_Mono" 

819 
"Tests/Misc_Poly" 

820 
"Tests/Small_Concrete" 

62725  821 
"Tests/Stream_Friends" 
62696  822 
"Tests/TLList_Friends" 
63190  823 
"Tests/Type_Class" 
62694  824 

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

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

827 
document_files "root.bib" "root.tex" 
48481  828 

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

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

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

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

833 
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

834 
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

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

836 
document_files "root.tex" 
48481  837 

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

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

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

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

841 
*} 
62479  842 
theories 
843 
Nonstandard_Analysis 

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

844 
document_files "root.tex" 
48481  845 

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

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

847 
options [document = false] 
48481  848 
theories NSPrimes 
849 

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

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

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

853 

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

854 
session "HOLMirabelleex" in "Mirabelle/ex" = "HOLMirabelle" + 
62354  855 
options [document = false, timeout = 60] 
49448
8a232a4e3fd8
reactivate HOLMirabelleex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
wenzelm
parents:
49439
diff
changeset

856 
theories Ex 
48481  857 

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

858 
session "HOLWordSMT_Examples" (timing) in SMT_Examples = "HOLWord" + 
62354  859 
options [document = false, quick_and_dirty] 
48481  860 
theories 
52722  861 
Boogie 
48481  862 
SMT_Examples 
863 
SMT_Word_Examples 

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

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

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

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

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

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

870 
"VCC_Max.certs" 
48481  871 

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

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

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

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

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

877 
options [document = false, spark_prv = false] 
48481  878 
theories 
879 
"Gcd/Greatest_Common_Divisor" 

880 

881 
"Liseq/Longest_Increasing_Subsequence" 

882 

883 
"RIPEMD160/F" 

884 
"RIPEMD160/Hash" 

885 
"RIPEMD160/K_L" 

886 
"RIPEMD160/K_R" 

887 
"RIPEMD160/R_L" 

888 
"RIPEMD160/Round" 

889 
"RIPEMD160/R_R" 

890 
"RIPEMD160/S_L" 

891 
"RIPEMD160/S_R" 

892 

893 
"Sqrt/Sqrt" 

894 
files 

895 
"Gcd/greatest_common_divisor/g_c_d.fdl" 

896 
"Gcd/greatest_common_divisor/g_c_d.rls" 

897 
"Gcd/greatest_common_divisor/g_c_d.siv" 

898 
"Liseq/liseq/liseq_length.fdl" 

899 
"Liseq/liseq/liseq_length.rls" 

900 
"Liseq/liseq/liseq_length.siv" 

901 
"RIPEMD160/rmd/f.fdl" 

902 
"RIPEMD160/rmd/f.rls" 

903 
"RIPEMD160/rmd/f.siv" 

904 
"RIPEMD160/rmd/hash.fdl" 

905 
"RIPEMD160/rmd/hash.rls" 

906 
"RIPEMD160/rmd/hash.siv" 

907 
"RIPEMD160/rmd/k_l.fdl" 

908 
"RIPEMD160/rmd/k_l.rls" 

909 
"RIPEMD160/rmd/k_l.siv" 

910 
"RIPEMD160/rmd/k_r.fdl" 

911 
"RIPEMD160/rmd/k_r.rls" 

912 
"RIPEMD160/rmd/k_r.siv" 

913 
"RIPEMD160/rmd/r_l.fdl" 

914 
"RIPEMD160/rmd/r_l.rls" 

915 
"RIPEMD160/rmd/r_l.siv" 

916 
"RIPEMD160/rmd/round.fdl" 

917 
"RIPEMD160/rmd/round.rls" 

918 
"RIPEMD160/rmd/round.siv" 

919 
"RIPEMD160/rmd/r_r.fdl" 

920 
"RIPEMD160/rmd/r_r.rls" 

921 
"RIPEMD160/rmd/r_r.siv" 

922 
"RIPEMD160/rmd/s_l.fdl" 

923 
"RIPEMD160/rmd/s_l.rls" 

924 
"RIPEMD160/rmd/s_l.siv" 

925 
"RIPEMD160/rmd/s_r.fdl" 

926 
"RIPEMD160/rmd/s_r.rls" 

927 
"RIPEMD160/rmd/s_r.siv" 

928 

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

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

930 
options [show_question_marks = false, spark_prv = false] 
48481  931 
theories 
932 
Example_Verification 

933 
VC_Principles 

934 
Reference 

935 
Complex_Types 

936 
files 

937 
"complex_types_app/initialize.fdl" 

938 
"complex_types_app/initialize.rls" 

939 
"complex_types_app/initialize.siv" 

940 
"loop_invariant/proc1.fdl" 

941 
"loop_invariant/proc1.rls" 

942 
"loop_invariant/proc1.siv" 

943 
"loop_invariant/proc2.fdl" 

944 
"loop_invariant/proc2.rls" 

945 
"loop_invariant/proc2.siv" 

946 
"simple_greatest_common_divisor/g_c_d.fdl" 

947 
"simple_greatest_common_divisor/g_c_d.rls" 

948 
"simple_greatest_common_divisor/g_c_d.siv" 

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

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

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

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

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

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

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

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

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

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

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

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

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

961 
"Simple_Gcd.ads" 
48481  962 

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

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

964 
options [document = false] 
48481  965 
theories MutabelleExtra 
966 

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

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

968 
options [document = false] 
48588  969 
theories 
48690  970 
Quickcheck_Examples 
971 
Quickcheck_Lattice_Examples 

972 
Completeness 

973 
Quickcheck_Interfaces 

63731
9f906a2eb0e7
added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
63643
diff
changeset

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

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

976 
Hotel_Example 
48598  977 
Quickcheck_Narrowing_Examples 
48588  978 

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

979 
session "HOLQuotient_Examples" (timing) in Quotient_Examples = HOL + 
48481  980 
description {* 
981 
Author: Cezary Kaliszyk and Christian Urban 

982 
*} 

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

983 
options [document = false] 
48481  984 
theories 
985 
DList 

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

986 
Quotient_FSet 
48481  987 
Quotient_Int 
988 
Quotient_Message 

989 
Lift_FSet 

990 
Lift_Set 

991 
Lift_Fun 

992 
Quotient_Rat 

993 
Lift_DList 

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

994 
Int_Pow 
60237  995 
Lifting_Code_Dt_Test 
48481  996 

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

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

998 
options [document = false] 
62354  999 
theories 
48481  1000 
Examples 
1001 
Predicate_Compile_Tests 

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

1002 
Predicate_Compile_Quickcheck_Examples 
48481  1003 
Specialisation_Examples 
48690  1004 
IMP_1 
1005 
IMP_2 

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

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

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

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

1010 
theories [condition = ISABELLE_SWIPL] 
48690  1011 
Code_Prolog_Examples 
1012 
Context_Free_Grammar_Example 

1013 
Hotel_Example_Prolog 

1014 
Lambda_Example 

1015 
List_Examples 

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

1016 
theories [condition = ISABELLE_SWIPL, quick_and_dirty] 
48690  1017 
Reg_Exp_Example 
48481  1018 

64551  1019 
session "HOLTypes_To_Sets" in Types_To_Sets = HOL + 
1020 
description {* 

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

1022 
*} 

1023 
options [document = false] 

1024 
theories 

1025 
Types_To_Sets 

1026 
"Examples/Prerequisites" 

1027 
"Examples/Finite" 

1028 
"Examples/T2_Spaces" 

1029 

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

1030 
session HOLCF (main timing) in HOLCF = HOL + 
48338  1031 
description {* 
1032 
Author: Franz Regensburger 

1033 
Author: Brian Huffman 

1034 

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

1036 
*} 

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

1037 
theories [document = false] 
48338  1038 
"~~/src/HOL/Library/Nat_Bijection" 
1039 
"~~/src/HOL/Library/Countable" 

48481  1040 
theories 
1041 
Plain_HOLCF 

1042 
Fixrec 

1043 
HOLCF 

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

1044 
document_files "root.tex" 
48481  1045 

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

1046 
session "HOLCFTutorial" in "HOLCF/Tutorial" = HOLCF + 
48481  1047 
theories 
1048 
Domain_ex 

1049 
Fixrec_ex 

1050 
New_Domain 

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

1051 
document_files "root.tex" 
48481  1052 

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

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

1054 
options [document = false] 
48481  1055 
theories HOLCF_Library 
1056 

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

1057 
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

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

1059 
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

1060 

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

1061 
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

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

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

1065 
document_files "root.tex" 
48338  1066 

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

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

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

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

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

1071 
options [document = false] 
48481  1072 
theories 
1073 
Dnat 

1074 
Dagstuhl 

1075 
Focus_ex 

1076 
Fix2 

1077 
Hoare 

1078 
Concurrency_Monad 

1079 
Loop 

1080 
Powerdomain_ex 

1081 
Domain_Proofs 

1082 
Letrec 

1083 
Pattern_Match 

1084 

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

1085 
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

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

1087 
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

1088 

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

1089 
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

1090 

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

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

1092 
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

1093 

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

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

1095 
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

1096 

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

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

1098 
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

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

1100 
options [document = false] 
48481  1101 
theories 
1102 
Fstreams 

1103 
FOCUS 

1104 
Buffer_adm 

1105 

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

1106 
session IOA (timing) in "HOLCF/IOA" = HOLCF + 
48481  1107 
description {* 
1108 
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

1109 
Copyright 1997 TU München 
48481  1110 

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

1111 
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

1112 

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

1113 
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

1114 
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

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

1117 
options [document = false] 
62008  1118 
theories "Abstraction" 
48481  1119 

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

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

1123 

1124 
The Alternating Bit Protocol performed in I/OAutomata. 

1125 
*} 

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

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

1129 
Spec 

48481  1130 

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

1131 
session "IOANTP" in "HOLCF/IOA/NTP" = IOA + 
48481  1132 
description {* 
1133 
Author: Tobias Nipkow & Konrad Slind 

1134 

1135 
A network transmission protocol, performed in the 

1136 
I/O automata formalization by Olaf Mueller. 

1137 
*} 

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

1138 
options [document = false] 
48481  1139 
theories Correctness 
1140 

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

1141 
session "IOAStorage" in "HOLCF/IOA/Storage" = IOA + 
48481  1142 
description {* 
1143 
Author: Olaf Mueller 

1144 

1145 
Memory storage case study. 

1146 
*} 

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

1147 
options [document = false] 
48481  1148 
theories Correctness 
1149 

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

1150 
session "IOAex" in "HOLCF/IOA/ex" = IOA + 
48481  1151 
description {* 
1152 
Author: Olaf Mueller 

1153 
*} 

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

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

1157 
TrivEx2 