author  haftmann 
Mon, 03 Oct 2016 14:37:06 +0200  
changeset 64015  c9f3a94cb825 
parent 63980  f8e556c8ad6f 
child 64282  261d42f0bfac 
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 
*} 
62354  21 
options [document = false, quick_and_dirty = false] 
52488
cd65ee49a8ba
discontinued system option "proofs"  global state of Proofterm.proofs is persistently compiled into HOLProofs image;
wenzelm
parents:
52424
diff
changeset

22 
theories Proofs (*sequential change of global flag!*) 
63827
b24d0e53dd03
option "checkpoint" helps to finetune global heap space management;
wenzelm
parents:
63763
diff
changeset

23 
theories List 
b24d0e53dd03
option "checkpoint" helps to finetune global heap space management;
wenzelm
parents:
63763
diff
changeset

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

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

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

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

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

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

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

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

32 
*} 
48481  33 
theories 
34 
Library 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

50 
Code_Char 
55447  51 
Code_Prolog 
48481  52 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

68 

69 
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

70 

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

71 
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

72 
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

73 
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

74 
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

75 

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

76 
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

77 
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

78 

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

79 
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

80 
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

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

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

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

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

86 
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

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

88 
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

89 

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

90 
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

91 
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

92 

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

93 
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

94 
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

95 

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

96 
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

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

98 
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

99 

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

100 
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

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

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

103 
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

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

107 
theories 

61935  108 
Nested_Datatype 
48481  109 
QuoDataType 
110 
QuoNestedDataType 

111 
Term 

112 
SList 

113 
ABexp 

114 
Tree 

115 
Ordinals 

116 
Sigma_Algebra 

117 
Comb 

118 
PropLog 

119 
Com 

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

120 
document_files "root.tex" 
48481  121 

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

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

126 
"~~/src/HOL/Library/Char_ord" 

127 
"~~/src/HOL/Library/List_lexord" 

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

48481  130 
theories 
131 
BExp 

132 
ASM 

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

138 
Sec_TypingT 

52726  139 
Def_Init_Big 
140 
Def_Init_Small 

141 
Fold 

48481  142 
Live 
143 
Live_True 

144 
Hoare_Examples 

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

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

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

150 
Collecting_Examples 
48481  151 
Abs_Int_Tests 
152 
Abs_Int1_parity 

153 
Abs_Int1_const 

154 
Abs_Int3 

155 
"Abs_Int_ITP/Abs_Int1_parity_ITP" 

156 
"Abs_Int_ITP/Abs_Int1_const_ITP" 

157 
"Abs_Int_ITP/Abs_Int3_ITP" 

158 
Procs_Dyn_Vars_Dyn 

159 
Procs_Stat_Vars_Dyn 

160 
Procs_Stat_Vars_Stat 

161 
C_like 

162 
OO 

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

163 
document_files "root.bib" "root.tex" 
48481  164 

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

165 
session "HOLIMPP" in IMPP = HOL + 
48481  166 
description {* 
167 
Author: David von Oheimb 

168 
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

169 

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

170 
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

171 

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

172 
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

173 
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

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

176 
options [document = false] 
48481  177 
theories EvenOdd 
178 

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

179 
session "HOLData_Structures" (timing) in Data_Structures = HOL + 
61203  180 
options [document_variants = document] 
181 
theories [document = false] 

182 
"Less_False" 

62706  183 
"~~/src/HOL/Library/Multiset" 
63643  184 
"~~/src/HOL/Library/Float" 
61203  185 
theories 
63829  186 
Balance 
61203  187 
Tree_Map 
61232  188 
AVL_Map 
61224  189 
RBT_Map 
61469
cd82b1023932
added 23 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
61368
diff
changeset

190 
Tree23_Map 
61514  191 
Tree234_Map 
61789  192 
Brother12_Map 
62130  193 
AA_Map 
61525  194 
Splay_Map 
62706  195 
Leftist_Heap 
61224  196 
document_files "root.tex" "root.bib" 
61203  197 

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

198 
session "HOLImport" in Import = HOL + 
48481  199 
theories HOL_Light_Maps 
200 
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 

201 

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

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

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

204 
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

205 
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

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

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

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

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

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

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

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

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

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

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

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

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

219 
"root.tex" 
48481  220 

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

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

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

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

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

225 
*} 
48481  226 
theories [document = false] 
227 
"~~/src/HOL/Library/Infinite_Set" 

228 
"~~/src/HOL/Library/Permutation" 

229 
theories 

230 
Fib 

231 
Factorization 

232 
Chinese 

233 
WilsonRuss 

234 
WilsonBij 

235 
Quadratic_Reciprocity 

236 
Primes 

237 
Pocklington 

58623  238 
document_files 
239 
"root.bib" 

240 
"root.tex" 

48481  241 

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

242 
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

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

244 
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

245 
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

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

248 
document_files "root.bib" "root.tex" 
48481  249 

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

250 
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

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

252 
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

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

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

256 
document_files "root.bib" "root.tex" 
48481  257 

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

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

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

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

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

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

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

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

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

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

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

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

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

277 
Code_Test_SMLNJ 
48481  278 

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

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

282 
Author: Jasmin Blanchette, TU Muenchen 

283 

284 
Testing Metis and Sledgehammer. 

285 
*} 

58423  286 
options [document = false] 
48481  287 
theories 
288 
Abstraction 

289 
Big_O 

290 
Binary_Tree 

291 
Clausification 

292 
Message 

293 
Proxies 

294 
Tarski 

295 
Trans_Closure 

296 
Sets 

297 

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

301 
Copyright 2009 

302 
*} 

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

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

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

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

309 

310 
The Isabelle Algebraic Library. 

311 
*} 

312 
theories [document = false] 

313 
(* Preliminaries from set and number theory *) 

314 
"~~/src/HOL/Library/FuncSet" 

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

315 
"~~/src/HOL/Number_Theory/Primes" 
48481  316 
"~~/src/HOL/Library/Permutation" 
317 
theories 

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

319 
(* Groups *) 

320 
FiniteProduct (* Product operator for commutative groups *) 

321 
Sylow (* Sylow's theorem *) 

322 
Bij (* Automorphism Groups *) 

323 

324 
(* Rings *) 

325 
Divisibility (* Rings *) 

326 
IntRing (* Ideals and residue classes *) 

327 
UnivPoly (* Polynomials *) 

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

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

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

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

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

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

333 
*} 
48481  334 
theories 
335 
Auth_Shared 

336 
Auth_Public 

337 
"Smartcard/Auth_Smartcard" 

338 
"Guard/Auth_Guard_Shared" 

339 
"Guard/Auth_Guard_Public" 

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

340 
document_files "root.tex" 
48481  341 

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

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

345 
Copyright 1998 University of Cambridge 

346 

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

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

350 
(*Basic metatheory*) 

351 
"UNITY_Main" 

352 

353 
(*Simple examples: no composition*) 

354 
"Simple/Deadlock" 

355 
"Simple/Common" 

356 
"Simple/Network" 

357 
"Simple/Token" 

358 
"Simple/Channel" 

359 
"Simple/Lift" 

360 
"Simple/Mutex" 

361 
"Simple/Reach" 

362 
"Simple/Reachability" 

363 

364 
(*Verifying security protocols using UNITY*) 

365 
"Simple/NSP_Bad" 

366 

367 
(*Example of composition*) 

368 
"Comp/Handshake" 

369 

370 
(*Universal properties examples*) 

371 
"Comp/Counter" 

372 
"Comp/Counterc" 

373 
"Comp/Priority" 

374 

375 
"Comp/TimerArray" 

376 
"Comp/Progress" 

377 

378 
"Comp/Alloc" 

379 
"Comp/AllocImpl" 

380 
"Comp/Client" 

381 

382 
(*obsolete*) 

383 
"ELT" 

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

384 
document_files "root.tex" 
48481  385 

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

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

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

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

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

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

393 
document_files "root.tex" 
48481  394 

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

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

399 
"~~/src/HOL/Library/Monad_Syntax" 

400 
"~~/src/HOL/Library/LaTeXsugar" 

401 
theories Imperative_HOL_ex 

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

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

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

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

407 
*} 

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

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

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

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

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

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

416 
XML_Data 
48481  417 

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

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

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

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

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

424 
"~~/src/HOL/Library/Code_Target_Numeral" 
48481  425 
"~~/src/HOL/Library/Monad_Syntax" 
426 
"~~/src/HOL/Number_Theory/Primes" 

427 
"~~/src/HOL/Library/State_Monad" 

428 
theories 

429 
Greatest_Common_Divisor 

430 
Warshall 

431 
Higman_Extraction 

432 
Pigeonhole 

433 
Euclid 

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

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

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

436 
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

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

438 
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

439 

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

440 
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

441 
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

442 

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

443 
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

444 
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

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

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

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

452 
StrongNorm 

453 
Standardization 

454 
WeakNorm 

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

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

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

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

460 

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

461 
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

462 

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

463 
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

464 
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

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

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

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

470 
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

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

472 
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

473 
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

474 
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

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

478 
theories 

479 
MicroJava 

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

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

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

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

483 
"root.tex" 
48481  484 

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

485 
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

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

487 
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

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

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

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

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

495 
AxSound 

496 
AxCompl 

497 
Trans 

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

499 
document_files "root.tex" 
48481  500 

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

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

503 
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

504 
Copyright 19941996 TU Muenchen 
48481  505 

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

506 
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

507 
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

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

510 
@inproceedings{NipkowSlindIOA, 

511 
author={Tobias Nipkow and Konrad Slind}, 

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

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

514 
publisher=Springer, 

515 
series=LNCS, 

516 
note={To appear}} 

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

518 

519 
and 

520 

521 
@inproceedings{MuellerNipkow, 

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

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

524 
booktitle={Proc.\ TACAS Workshop}, 

525 
organization={Aarhus University, BRICS report}, 

526 
year=1995} 

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

528 
*} 

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

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

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

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

535 

536 
Basic theory of lattices and orders. 

537 
*} 

538 
theories CompleteLattice 

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

539 
document_files "root.tex" 
48481  540 

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

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

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

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

544 
*} 
48481  545 
theories [document = false] 
546 
"~~/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

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

550 
Normalization_by_Evaluation 

551 
Hebrew 

552 
Chinese 

553 
Serbian 

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

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

556 
Cartouche_Examples 
48481  557 
theories 
59090  558 
Commands 
57507  559 
Adhoc_Overloading_Examples 
48481  560 
Iff_Oracle 
561 
Coercion_Examples 

562 
Abstract_NAT 

563 
Guess 

62999  564 
Functions 
48481  565 
Induction_Schema 
566 
LocaleTest2 

567 
Records 

568 
While_Combinator_Example 

569 
MonoidGroup 

570 
BinEx 

571 
Hex_Bin_Examples 

572 
Antiquote 

573 
Multiquote 

574 
PER 

575 
NatSum 

576 
ThreeDivides 

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

577 
Cubic_Quartic 
59739  578 
Pythagoras 
48481  579 
Intuitionistic 
580 
CTL 

581 
Arith_Examples 

582 
Tree23 

58644  583 
Bubblesort 
48481  584 
MergeSort 
585 
Lagrange 

586 
Groebner_Examples 

587 
Unification 

588 
Primrec 

589 
Tarski 

590 
Classical 

591 
Set_Theory 

592 
Termination 

593 
Coherent 

594 
PresburgerEx 

51093  595 
Reflection_Examples 
48481  596 
Sqrt 
597 
Sqrt_Script 

61368  598 
Transfer_Debug 
48481  599 
Transfer_Ex 
600 
Transfer_Int_Nat 

56922  601 
Transitive_Closure_Table_Ex 
48481  602 
HarmonicSeries 
603 
Refute_Examples 

604 
Execute_Choice 

605 
Gauge_Integration 

606 
Dedekind_Real 

607 
Quicksort 

608 
Birthday_Paradox 

609 
List_to_Set_Comprehension_Examples 

610 
Seq 

611 
Simproc_Tests 

612 
Executable_Relation 

613 
FinFunPred 

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

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

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

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

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

628 
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

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

630 
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

631 
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

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

633 
document_files "root.bib" "root.tex" 
48481  634 

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

635 
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

636 
description {* 
61935  637 
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

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

642 
"../Number_Theory/Primes" 

643 
theories 

61939  644 
Knaster_Tarski 
645 
Peirce 

646 
Drinker 

48481  647 
Cantor 
61939  648 
Structured_Statements 
649 
Basic_Logic 

48481  650 
Expr_Compiler 
651 
Fibonacci 

652 
Group 

653 
Group_Context 

654 
Group_Notepad 

655 
Hoare_Ex 

656 
Mutilated_Checkerboard 

657 
Puzzle 

658 
Summation 

61935  659 
First_Order_Logic 
660 
Higher_Order_Logic 

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

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

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

663 
"root.tex" 
48481  664 

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

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

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

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

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

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

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

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

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

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

674 

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

675 
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

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

677 
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

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

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

681 
document_files "root.tex" 
48481  682 

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

683 
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

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

685 
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

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

688 
document_files "root.tex" 
48481  689 

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

690 
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

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

692 
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

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

694 
options [document = false] 
48481  695 
theories TLA 
696 

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

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

698 
options [document = false] 
48481  699 
theories Inc 
700 

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

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

702 
options [document = false] 
48481  703 
theories DBuffer 
704 

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

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

706 
options [document = false] 
48481  707 
theories MemoryImplementation 
708 

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

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

712 
Author: Nik Sultana, University of Cambridge 

713 
Copyright 2011 

714 

715 
TPTPrelated extensions. 

716 
*} 

62354  717 
options [document = false] 
48481  718 
theories 
719 
ATP_Theory_Export 

720 
MaSh_Eval 

721 
TPTP_Interpret 

722 
THF_Arith 

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

723 
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

724 
theories 
48481  725 
ATP_Problem_Import 
726 

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

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

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

731 
"root.tex" 
48481  732 

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

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

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

736 

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

737 
session "HOLProbability" (timing) in "Probability" = "HOLAnalysis" + 
48481  738 
theories [document = false] 
739 
"~~/src/HOL/Library/Countable" 

740 
"~~/src/HOL/Library/Permutation" 

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

743 
"~~/src/HOL/Library/Finite_Map" 
48481  744 
theories 
745 
Probability 

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

746 
document_files "root.tex" 
48481  747 

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

748 
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

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

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

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

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

753 

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

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

755 
options [document = false] 
48481  756 
theories Nominal 
757 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

782 
VC_Condition 
48481  783 

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

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

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

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

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

788 
options [document = false] 
59747  789 
theories 
790 
Cardinals 

791 
Bounded_Set 

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

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

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

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

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

796 

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

797 
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

798 
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

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

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

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

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

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

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

806 
TreeFsetI 
49872  807 
"Derivation_Trees/Gram_Lang" 
808 
"Derivation_Trees/Parallel" 

50517  809 
Koenig 
60921  810 
Lift_BNF 
61745  811 
Milner_Tofte 
54961  812 
Stream_Processor 
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset

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

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

817 

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

818 
session "HOLCorec_Examples" (timing) in Corec_Examples = HOL + 
62694  819 
description {* 
820 
Corecursion Examples. 

821 
*} 

822 
options [document = false] 

823 
theories 

824 
LFilter 

62734  825 
Paper_Examples 
62694  826 
Stream_Processor 
62696  827 
"Tests/Simple_Nesting" 
828 
theories [quick_and_dirty] 

829 
"Tests/GPV_Bare_Bones" 

830 
"Tests/Merge_D" 

831 
"Tests/Merge_Poly" 

832 
"Tests/Misc_Mono" 

833 
"Tests/Misc_Poly" 

834 
"Tests/Small_Concrete" 

62725  835 
"Tests/Stream_Friends" 
62696  836 
"Tests/TLList_Friends" 
63190  837 
"Tests/Type_Class" 
62694  838 

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

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

841 
document_files "root.bib" "root.tex" 
48481  842 

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

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

844 
options [document = false] 
48481  845 
theories WordExamples 
846 

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

847 
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

848 
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

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

850 
document_files "root.tex" 
48481  851 

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

852 
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

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

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

855 
*} 
62479  856 
theories 
857 
Nonstandard_Analysis 

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

858 
document_files "root.tex" 
48481  859 

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

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

861 
options [document = false] 
48481  862 
theories NSPrimes 
863 

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

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

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

867 

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

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

870 
theories Ex 
48481  871 

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

872 
session "HOLWordSMT_Examples" (timing) in SMT_Examples = "HOLWord" + 
62354  873 
options [document = false, quick_and_dirty] 
48481  874 
theories 
52722  875 
Boogie 
48481  876 
SMT_Examples 
877 
SMT_Word_Examples 

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

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

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

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

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

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

884 
"VCC_Max.certs" 
48481  885 

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

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

887 
options [document = false] 
48481  888 
theories SPARK 
889 

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

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

891 
options [document = false, spark_prv = false] 
48481  892 
theories 
893 
"Gcd/Greatest_Common_Divisor" 

894 

895 
"Liseq/Longest_Increasing_Subsequence" 

896 

897 
"RIPEMD160/F" 

898 
"RIPEMD160/Hash" 

899 
"RIPEMD160/K_L" 

900 
"RIPEMD160/K_R" 

901 
"RIPEMD160/R_L" 

902 
"RIPEMD160/Round" 

903 
"RIPEMD160/R_R" 

904 
"RIPEMD160/S_L" 

905 
"RIPEMD160/S_R" 

906 

907 
"Sqrt/Sqrt" 

908 
files 

909 
"Gcd/greatest_common_divisor/g_c_d.fdl" 

910 
"Gcd/greatest_common_divisor/g_c_d.rls" 

911 
"Gcd/greatest_common_divisor/g_c_d.siv" 

912 
"Liseq/liseq/liseq_length.fdl" 

913 
"Liseq/liseq/liseq_length.rls" 

914 
"Liseq/liseq/liseq_length.siv" 

915 
"RIPEMD160/rmd/f.fdl" 

916 
"RIPEMD160/rmd/f.rls" 

917 
"RIPEMD160/rmd/f.siv" 

918 
"RIPEMD160/rmd/hash.fdl" 

919 
"RIPEMD160/rmd/hash.rls" 

920 
"RIPEMD160/rmd/hash.siv" 

921 
"RIPEMD160/rmd/k_l.fdl" 

922 
"RIPEMD160/rmd/k_l.rls" 

923 
"RIPEMD160/rmd/k_l.siv" 

924 
"RIPEMD160/rmd/k_r.fdl" 

925 
"RIPEMD160/rmd/k_r.rls" 

926 
"RIPEMD160/rmd/k_r.siv" 

927 
"RIPEMD160/rmd/r_l.fdl" 

928 
"RIPEMD160/rmd/r_l.rls" 

929 
"RIPEMD160/rmd/r_l.siv" 

930 
"RIPEMD160/rmd/round.fdl" 

931 
"RIPEMD160/rmd/round.rls" 

932 
"RIPEMD160/rmd/round.siv" 

933 
"RIPEMD160/rmd/r_r.fdl" 

934 
"RIPEMD160/rmd/r_r.rls" 

935 
"RIPEMD160/rmd/r_r.siv" 

936 
"RIPEMD160/rmd/s_l.fdl" 

937 
"RIPEMD160/rmd/s_l.rls" 

938 
"RIPEMD160/rmd/s_l.siv" 

939 
"RIPEMD160/rmd/s_r.fdl" 

940 
"RIPEMD160/rmd/s_r.rls" 

941 
"RIPEMD160/rmd/s_r.siv" 

942 

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

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

944 
options [show_question_marks = false, spark_prv = false] 
48481  945 
theories 
946 
Example_Verification 

947 
VC_Principles 

948 
Reference 

949 
Complex_Types 

950 
files 

951 
"complex_types_app/initialize.fdl" 

952 
"complex_types_app/initialize.rls" 

953 
"complex_types_app/initialize.siv" 

954 
"loop_invariant/proc1.fdl" 

955 
"loop_invariant/proc1.rls" 

956 
"loop_invariant/proc1.siv" 

957 
"loop_invariant/proc2.fdl" 

958 
"loop_invariant/proc2.rls" 

959 
"loop_invariant/proc2.siv" 

960 
"simple_greatest_common_divisor/g_c_d.fdl" 

961 
"simple_greatest_common_divisor/g_c_d.rls" 

962 
"simple_greatest_common_divisor/g_c_d.siv" 

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

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

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

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

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

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

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

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

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

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

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

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

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

975 
"Simple_Gcd.ads" 
48481  976 

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

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

978 
options [document = false] 
48481  979 
theories MutabelleExtra 
980 

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

981 
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

982 
options [document = false] 
48588  983 
theories 
48690  984 
Quickcheck_Examples 
985 
Quickcheck_Lattice_Examples 

986 
Completeness 

987 
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

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

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

990 
Hotel_Example 
48598  991 
Quickcheck_Narrowing_Examples 
48588  992 

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

993 
session "HOLQuotient_Examples" (timing) in Quotient_Examples = HOL + 
48481  994 
description {* 
995 
Author: Cezary Kaliszyk and Christian Urban 

996 
*} 

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

997 
options [document = false] 
48481  998 
theories 
999 
DList 

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

1000 
Quotient_FSet 
48481  1001 
Quotient_Int 
1002 
Quotient_Message 

1003 
Lift_FSet 

1004 
Lift_Set 

1005 
Lift_Fun 

1006 
Quotient_Rat 

1007 
Lift_DList 

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

1008 
Int_Pow 
60237  1009 
Lifting_Code_Dt_Test 
48481  1010 

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

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

1012 
options [document = false] 
62354  1013 
theories 
48481  1014 
Examples 
1015 
Predicate_Compile_Tests 

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

1016 
Predicate_Compile_Quickcheck_Examples 
48481  1017 
Specialisation_Examples 
48690  1018 
IMP_1 
1019 
IMP_2 

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

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

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

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

1024 
theories [condition = ISABELLE_SWIPL] 
48690  1025 
Code_Prolog_Examples 
1026 
Context_Free_Grammar_Example 

1027 
Hotel_Example_Prolog 

1028 
Lambda_Example 

1029 
List_Examples 

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

1030 
theories [condition = ISABELLE_SWIPL, quick_and_dirty] 
48690  1031 
Reg_Exp_Example 
48481  1032 

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

1033 
session HOLCF (main timing) in HOLCF = HOL + 
48338  1034 
description {* 
1035 
Author: Franz Regensburger 

1036 
Author: Brian Huffman 

1037 

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

1039 
*} 

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

1040 
theories [document = false] 
48338  1041 
"~~/src/HOL/Library/Nat_Bijection" 
1042 
"~~/src/HOL/Library/Countable" 

48481  1043 
theories 
1044 
Plain_HOLCF 

1045 
Fixrec 

1046 
HOLCF 

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

1047 
document_files "root.tex" 
48481  1048 

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

1049 
session "HOLCFTutorial" in "HOLCF/Tutorial" = HOLCF + 
48481  1050 
theories 
1051 
Domain_ex 

1052 
Fixrec_ex 

1053 
New_Domain 

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

1054 
document_files "root.tex" 
48481  1055 

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

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

1057 
options [document = false] 
48481  1058 
theories HOLCF_Library 
1059 

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

1060 
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

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

1062 
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

1063 

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

1064 
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

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

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

1068 
document_files "root.tex" 
48338  1069 

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

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

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

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

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

1074 
options [document = false] 
48481  1075 
theories 
1076 
Dnat 

1077 
Dagstuhl 

1078 
Focus_ex 

1079 
Fix2 

1080 
Hoare 

1081 
Concurrency_Monad 

1082 
Loop 

1083 
Powerdomain_ex 

1084 
Domain_Proofs 

1085 
Letrec 

1086 
Pattern_Match 

1087 

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

1088 
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

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

1090 
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

1091 

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

1092 
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

1093 

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

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

1095 
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

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

1098 
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

1099 

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

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

1101 
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

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

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

1106 
FOCUS 

1107 
Buffer_adm 

1108 

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

1109 
session IOA (timing) in "HOLCF/IOA" = HOLCF + 
48481  1110 
description {* 
1111 
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

1112 
Copyright 1997 TU München 
48481  1113 

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

1114 
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

1115 

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

1116 
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

1117 
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

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

1120 
options [document = false] 
62008  1121 
theories "Abstraction" 
48481  1122 

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

1123 
session "IOAABP" in "HOLCF/IOA/ABP" = IOA + 
48481  1124 
description {* 
1125 
Author: Olaf Mueller 

1126 

1127 
The Alternating Bit Protocol performed in I/OAutomata. 

1128 
*} 

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

1129 
options [document = false] 
59503  1130 
theories 
1131 
Correctness 

1132 
Spec 

48481  1133 

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

1134 
session "IOANTP" in "HOLCF/IOA/NTP" = IOA + 
48481  1135 
description {* 
1136 
Author: Tobias Nipkow & Konrad Slind 

1137 

1138 
A network transmission protocol, performed in the 

1139 
I/O automata formalization by Olaf Mueller. 

1140 
*} 

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

1141 
options [document = false] 
48481  1142 
theories Correctness 
1143 

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

1144 
session "IOAStorage" in "HOLCF/IOA/Storage" = IOA + 
48481  1145 
description {* 
1146 
Author: Olaf Mueller 

1147 

1148 
Memory storage case study. 

1149 
*} 

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

1150 
options [document = false] 
48481  1151 
theories Correctness 
1152 

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

1153 
session "IOAex" in "HOLCF/IOA/ex" = IOA + 
48481  1154 
description {* 
1155 
Author: Olaf Mueller 

1156 
*} 

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

1157 
options [document = false] 
48481  1158 
theories 
1159 
TrivEx 

1160 
TrivEx2 