author | wenzelm |
Tue, 12 Mar 2013 21:59:48 +0100 | |
changeset 51403 | 2ff3a5589b05 |
parent 51397 | 03b586ee5930 |
child 51421 | b5d559b101d9 |
permissions | -rw-r--r-- |
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 + |
48338 | 4 |
description {* Classical Higher-order Logic *} |
5 |
options [document_graph] |
|
6 |
theories Complex_Main |
|
48901
5e0455e29339
more basic file dependencies -- no load command here;
wenzelm
parents:
48765
diff
changeset
|
7 |
files |
5e0455e29339
more basic file dependencies -- no load command here;
wenzelm
parents:
48765
diff
changeset
|
8 |
"Tools/Quickcheck/Narrowing_Engine.hs" |
5e0455e29339
more basic file dependencies -- no load command here;
wenzelm
parents:
48765
diff
changeset
|
9 |
"Tools/Quickcheck/PNF_Narrowing_Engine.hs" |
5e0455e29339
more basic file dependencies -- no load command here;
wenzelm
parents:
48765
diff
changeset
|
10 |
"document/root.bib" |
5e0455e29339
more basic file dependencies -- no load command here;
wenzelm
parents:
48765
diff
changeset
|
11 |
"document/root.tex" |
48338 | 12 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
13 |
session "HOL-Proofs" = Pure + |
48509 | 14 |
description {* HOL-Main with explicit proof terms *} |
50988 | 15 |
options [document = false, proofs = 2] |
48338 | 16 |
theories Main |
48901
5e0455e29339
more basic file dependencies -- no load command here;
wenzelm
parents:
48765
diff
changeset
|
17 |
files |
5e0455e29339
more basic file dependencies -- no load command here;
wenzelm
parents:
48765
diff
changeset
|
18 |
"Tools/Quickcheck/Narrowing_Engine.hs" |
5e0455e29339
more basic file dependencies -- no load command here;
wenzelm
parents:
48765
diff
changeset
|
19 |
"Tools/Quickcheck/PNF_Narrowing_Engine.hs" |
48338 | 20 |
|
50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset
|
21 |
session "HOL-Library" (main) in Library = HOL + |
48481 | 22 |
description {* Classical Higher-order Logic -- batteries included *} |
23 |
theories |
|
24 |
Library |
|
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
25 |
(*conflicting type class instantiations*) |
48481 | 26 |
List_lexord |
27 |
Sublist_Order |
|
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51093
diff
changeset
|
28 |
Product_Lexorder |
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51093
diff
changeset
|
29 |
Product_Order |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
30 |
Finite_Lattice |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
31 |
(*data refinements and dependent applications*) |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
32 |
AList_Mapping |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
33 |
Code_Binary_Nat |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
34 |
Code_Char |
48721 | 35 |
(* Code_Prolog FIXME cf. 76965c356d2a *) |
48481 | 36 |
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
|
37 |
Code_Target_Numeral |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
38 |
DAList |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
39 |
RBT_Mapping |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
40 |
RBT_Set |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
41 |
(*legacy tools*) |
49985
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49932
diff
changeset
|
42 |
Refute |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
43 |
Old_Recdef |
48932
c6e679443adc
actual use of (sos remote_csdp) via ISABELLE_FULL_TEST;
wenzelm
parents:
48901
diff
changeset
|
44 |
theories [condition = ISABELLE_FULL_TEST] |
c6e679443adc
actual use of (sos remote_csdp) via ISABELLE_FULL_TEST;
wenzelm
parents:
48901
diff
changeset
|
45 |
Sum_of_Squares_Remote |
48481 | 46 |
files "document/root.bib" "document/root.tex" |
47 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
48 |
session "HOL-Hahn_Banach" in Hahn_Banach = HOL + |
48481 | 49 |
description {* |
50 |
Author: Gertrud Bauer, TU Munich |
|
51 |
||
52 |
The Hahn-Banach 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
|
53 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
54 |
This is the proof of the Hahn-Banach 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
|
55 |
following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
56 |
theorem is one of the fundamental theorems of functioal analysis. It is a |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
57 |
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
|
58 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
59 |
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
|
60 |
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
|
61 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
62 |
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
|
63 |
subspaces (not only one-dimensional 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
|
64 |
continous linearform on the whole vectorspace. |
48481 | 65 |
*} |
66 |
options [document_graph] |
|
67 |
theories Hahn_Banach |
|
68 |
files "document/root.bib" "document/root.tex" |
|
69 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
70 |
session "HOL-Induct" 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
|
71 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
72 |
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
|
73 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
74 |
Comb proves the Church-Rosser 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
|
75 |
http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz). |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
76 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
77 |
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
|
78 |
http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz). |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
79 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
80 |
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
|
81 |
(see |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
82 |
HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz). |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
83 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
84 |
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
|
85 |
mutually recursive relations. |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
86 |
*} |
48481 | 87 |
theories [quick_and_dirty] |
88 |
Common_Patterns |
|
89 |
theories |
|
90 |
QuoDataType |
|
91 |
QuoNestedDataType |
|
92 |
Term |
|
93 |
SList |
|
94 |
ABexp |
|
95 |
Tree |
|
96 |
Ordinals |
|
97 |
Sigma_Algebra |
|
98 |
Comb |
|
99 |
PropLog |
|
100 |
Com |
|
101 |
files "document/root.tex" |
|
102 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
103 |
session "HOL-IMP" in IMP = HOL + |
50870
b8606dd29783
hardwired document_variants, to prevent HOL-IMP's \snip choking on macros from isabellestags.sty;
wenzelm
parents:
50844
diff
changeset
|
104 |
options [document_graph, document_variants=document] |
48481 | 105 |
theories [document = false] |
106 |
"~~/src/HOL/ex/Interpretation_with_Defs" |
|
107 |
"~~/src/HOL/Library/While_Combinator" |
|
108 |
"~~/src/HOL/Library/Char_ord" |
|
109 |
"~~/src/HOL/Library/List_lexord" |
|
110 |
theories |
|
111 |
BExp |
|
112 |
ASM |
|
50050 | 113 |
Finite_Reachable |
48481 | 114 |
Denotation |
115 |
Comp_Rev |
|
116 |
Poly_Types |
|
117 |
Sec_Typing |
|
118 |
Sec_TypingT |
|
50161 | 119 |
Def_Init_Sound_Big |
120 |
Def_Init_Sound_Small |
|
48481 | 121 |
Live |
122 |
Live_True |
|
123 |
Hoare_Examples |
|
124 |
VC |
|
125 |
HoareT |
|
126 |
Collecting1 |
|
48765
fb1ed5230abc
special code with lists no longer necessary, use sets
nipkow
parents:
48738
diff
changeset
|
127 |
Collecting_Examples |
48481 | 128 |
Abs_Int_Tests |
129 |
Abs_Int1_parity |
|
130 |
Abs_Int1_const |
|
131 |
Abs_Int3 |
|
132 |
"Abs_Int_ITP/Abs_Int1_parity_ITP" |
|
133 |
"Abs_Int_ITP/Abs_Int1_const_ITP" |
|
134 |
"Abs_Int_ITP/Abs_Int3_ITP" |
|
135 |
"Abs_Int_Den/Abs_Int_den2" |
|
136 |
Procs_Dyn_Vars_Dyn |
|
137 |
Procs_Stat_Vars_Dyn |
|
138 |
Procs_Stat_Vars_Stat |
|
139 |
C_like |
|
140 |
OO |
|
141 |
Fold |
|
142 |
files "document/root.bib" "document/root.tex" |
|
143 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
144 |
session "HOL-IMPP" in IMPP = HOL + |
48481 | 145 |
description {* |
146 |
Author: David von Oheimb |
|
147 |
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
|
148 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
149 |
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
|
150 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
151 |
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
|
152 |
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
|
153 |
Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). |
48481 | 154 |
*} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
155 |
options [document = false] |
48481 | 156 |
theories EvenOdd |
157 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
158 |
session "HOL-Import" in Import = HOL + |
48481 | 159 |
options [document_graph] |
160 |
theories HOL_Light_Maps |
|
161 |
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import |
|
162 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
163 |
session "HOL-Number_Theory" in Number_Theory = HOL + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
164 |
options [document = false] |
48481 | 165 |
theories Number_Theory |
166 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
167 |
session "HOL-Old_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
|
168 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
169 |
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
|
170 |
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
|
171 |
*} |
48481 | 172 |
options [document_graph] |
173 |
theories [document = false] |
|
174 |
"~~/src/HOL/Library/Infinite_Set" |
|
175 |
"~~/src/HOL/Library/Permutation" |
|
176 |
theories |
|
177 |
Fib |
|
178 |
Factorization |
|
179 |
Chinese |
|
180 |
WilsonRuss |
|
181 |
WilsonBij |
|
182 |
Quadratic_Reciprocity |
|
183 |
Primes |
|
184 |
Pocklington |
|
185 |
files "document/root.tex" |
|
186 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
187 |
session "HOL-Hoare" 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
|
188 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
189 |
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
|
190 |
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
|
191 |
*} |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
192 |
|
48481 | 193 |
theories Hoare |
194 |
files "document/root.bib" "document/root.tex" |
|
195 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
196 |
session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL + |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
197 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
198 |
Verification of shared-variable imperative programs a la Owicki-Gries. |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
199 |
(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
|
200 |
*} |
48481 | 201 |
options [document_graph] |
202 |
theories Hoare_Parallel |
|
203 |
files "document/root.bib" "document/root.tex" |
|
204 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
205 |
session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" + |
48481 | 206 |
options [document = false, document_graph = false, browser_info = false] |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
207 |
theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Generate_Pretty_Char |
48481 | 208 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
209 |
session "HOL-Metis_Examples" in Metis_Examples = HOL + |
48481 | 210 |
description {* |
211 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
212 |
Author: Jasmin Blanchette, TU Muenchen |
|
213 |
||
214 |
Testing Metis and Sledgehammer. |
|
215 |
*} |
|
48679 | 216 |
options [timeout = 3600, document = false] |
48481 | 217 |
theories |
218 |
Abstraction |
|
219 |
Big_O |
|
220 |
Binary_Tree |
|
221 |
Clausification |
|
222 |
Message |
|
223 |
Proxies |
|
224 |
Tarski |
|
225 |
Trans_Closure |
|
226 |
Sets |
|
227 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
228 |
session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL + |
48481 | 229 |
description {* |
230 |
Author: Jasmin Blanchette, TU Muenchen |
|
231 |
Copyright 2009 |
|
232 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
233 |
options [document = false] |
48481 | 234 |
theories [quick_and_dirty] Nitpick_Examples |
235 |
||
50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset
|
236 |
session "HOL-Algebra" (main) in Algebra = HOL + |
48481 | 237 |
description {* |
238 |
Author: Clemens Ballarin, started 24 September 1999 |
|
239 |
||
240 |
The Isabelle Algebraic Library. |
|
241 |
*} |
|
242 |
options [document_graph] |
|
243 |
theories [document = false] |
|
244 |
(* Preliminaries from set and number theory *) |
|
245 |
"~~/src/HOL/Library/FuncSet" |
|
246 |
"~~/src/HOL/Old_Number_Theory/Primes" |
|
247 |
"~~/src/HOL/Library/Binomial" |
|
248 |
"~~/src/HOL/Library/Permutation" |
|
249 |
theories |
|
250 |
(*** New development, based on explicit structures ***) |
|
251 |
(* Groups *) |
|
252 |
FiniteProduct (* Product operator for commutative groups *) |
|
253 |
Sylow (* Sylow's theorem *) |
|
254 |
Bij (* Automorphism Groups *) |
|
255 |
||
256 |
(* Rings *) |
|
257 |
Divisibility (* Rings *) |
|
258 |
IntRing (* Ideals and residue classes *) |
|
259 |
UnivPoly (* Polynomials *) |
|
260 |
theories [document = false] |
|
261 |
(*** Old development, based on axiomatic type classes ***) |
|
262 |
"abstract/Abstract" (*The ring theory*) |
|
263 |
"poly/Polynomial" (*The full theory*) |
|
264 |
files "document/root.bib" "document/root.tex" |
|
265 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
266 |
session "HOL-Auth" in Auth = HOL + |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
267 |
description {* A new approach to verifying authentication protocols. *} |
48481 | 268 |
options [document_graph] |
269 |
theories |
|
270 |
Auth_Shared |
|
271 |
Auth_Public |
|
272 |
"Smartcard/Auth_Smartcard" |
|
273 |
"Guard/Auth_Guard_Shared" |
|
274 |
"Guard/Auth_Guard_Public" |
|
275 |
files "document/root.tex" |
|
276 |
||
51236
f301ad90c48b
more explicit session dependency, for improved parallel performance of HOL-UNITY test session -- NB: separate 'theories' sections are sequential;
wenzelm
parents:
51161
diff
changeset
|
277 |
session "HOL-UNITY" in UNITY = "HOL-Auth" + |
48481 | 278 |
description {* |
279 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
280 |
Copyright 1998 University of Cambridge |
|
281 |
||
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
282 |
Verifying security protocols using Chandy and Misra's UNITY formalism. |
48481 | 283 |
*} |
284 |
options [document_graph] |
|
285 |
theories |
|
286 |
(*Basic meta-theory*) |
|
287 |
"UNITY_Main" |
|
288 |
||
289 |
(*Simple examples: no composition*) |
|
290 |
"Simple/Deadlock" |
|
291 |
"Simple/Common" |
|
292 |
"Simple/Network" |
|
293 |
"Simple/Token" |
|
294 |
"Simple/Channel" |
|
295 |
"Simple/Lift" |
|
296 |
"Simple/Mutex" |
|
297 |
"Simple/Reach" |
|
298 |
"Simple/Reachability" |
|
299 |
||
300 |
(*Verifying security protocols using UNITY*) |
|
301 |
"Simple/NSP_Bad" |
|
302 |
||
303 |
(*Example of composition*) |
|
304 |
"Comp/Handshake" |
|
305 |
||
306 |
(*Universal properties examples*) |
|
307 |
"Comp/Counter" |
|
308 |
"Comp/Counterc" |
|
309 |
"Comp/Priority" |
|
310 |
||
311 |
"Comp/TimerArray" |
|
312 |
"Comp/Progress" |
|
313 |
||
314 |
"Comp/Alloc" |
|
315 |
"Comp/AllocImpl" |
|
316 |
"Comp/Client" |
|
317 |
||
318 |
(*obsolete*) |
|
319 |
"ELT" |
|
320 |
files "document/root.tex" |
|
321 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
322 |
session "HOL-Unix" in Unix = HOL + |
48481 | 323 |
options [print_mode = "no_brackets,no_type_brackets"] |
324 |
theories Unix |
|
325 |
files "document/root.bib" "document/root.tex" |
|
326 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
327 |
session "HOL-ZF" in ZF = HOL + |
48481 | 328 |
theories MainZF Games |
329 |
files "document/root.tex" |
|
330 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
331 |
session "HOL-Imperative_HOL" in Imperative_HOL = HOL + |
48481 | 332 |
options [document_graph, print_mode = "iff,no_brackets"] |
333 |
theories [document = false] |
|
334 |
"~~/src/HOL/Library/Countable" |
|
335 |
"~~/src/HOL/Library/Monad_Syntax" |
|
336 |
"~~/src/HOL/Library/LaTeXsugar" |
|
337 |
theories Imperative_HOL_ex |
|
338 |
files "document/root.bib" "document/root.tex" |
|
339 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
340 |
session "HOL-Decision_Procs" in Decision_Procs = HOL + |
48496
a7eed34cf219
added condition = ISABELLE_POLYML according to no-smlnj targets in IsaMakefile;
wenzelm
parents:
48493
diff
changeset
|
341 |
options [condition = ISABELLE_POLYML, document = false] |
48481 | 342 |
theories Decision_Procs |
343 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
344 |
session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
345 |
options [document = false, proofs = 2, parallel_proofs = 0] |
48481 | 346 |
theories Hilbert_Classical |
347 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
348 |
session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" + |
48481 | 349 |
description {* Examples for program extraction in Higher-Order Logic *} |
48496
a7eed34cf219
added condition = ISABELLE_POLYML according to no-smlnj targets in IsaMakefile;
wenzelm
parents:
48493
diff
changeset
|
350 |
options [condition = ISABELLE_POLYML, proofs = 2, parallel_proofs = 0] |
48481 | 351 |
theories [document = false] |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51115
diff
changeset
|
352 |
"~~/src/HOL/Library/Code_Target_Numeral" |
48481 | 353 |
"~~/src/HOL/Library/Monad_Syntax" |
354 |
"~~/src/HOL/Number_Theory/Primes" |
|
355 |
"~~/src/HOL/Number_Theory/UniqueFactorization" |
|
356 |
"~~/src/HOL/Library/State_Monad" |
|
357 |
theories |
|
358 |
Greatest_Common_Divisor |
|
359 |
Warshall |
|
360 |
Higman_Extraction |
|
361 |
Pigeonhole |
|
362 |
Euclid |
|
363 |
files "document/root.bib" "document/root.tex" |
|
364 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
365 |
session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" + |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
366 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
367 |
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
|
368 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
369 |
This session defines lambda-calculus 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
|
370 |
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
|
371 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
372 |
The paper "More Church-Rosser 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
|
373 |
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
|
374 |
*} |
48481 | 375 |
options [document_graph, print_mode = "no_brackets", proofs = 2, parallel_proofs = 0] |
376 |
theories [document = false] |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51115
diff
changeset
|
377 |
"~~/src/HOL/Library/Code_Target_Int" |
48481 | 378 |
theories |
379 |
Eta |
|
380 |
StrongNorm |
|
381 |
Standardization |
|
382 |
WeakNorm |
|
383 |
files "document/root.bib" "document/root.tex" |
|
384 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
385 |
session "HOL-Prolog" in Prolog = HOL + |
48481 | 386 |
description {* |
387 |
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
|
388 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
389 |
A bare-bones implementation of Lambda-Prolog. |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
390 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
391 |
This is a simple exploratory implementation of Lambda-Prolog in HOL, |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
392 |
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
|
393 |
a little functional language and its type system. |
48481 | 394 |
*} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
395 |
options [document = false] |
48481 | 396 |
theories Test Type |
397 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
398 |
session "HOL-MicroJava" 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
|
399 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
400 |
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
|
401 |
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
|
402 |
bytecode verifier, including proofs of type-safety. |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
403 |
*} |
48481 | 404 |
options [document_graph] |
405 |
theories [document = false] "~~/src/HOL/Library/While_Combinator" |
|
406 |
theories MicroJava |
|
407 |
files |
|
408 |
"document/introduction.tex" |
|
409 |
"document/root.bib" |
|
410 |
"document/root.tex" |
|
411 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
412 |
session "HOL-MicroJava-skip_proofs" in MicroJava = HOL + |
48636 | 413 |
options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs, quick_and_dirty] |
414 |
theories MicroJava |
|
415 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
416 |
session "HOL-NanoJava" 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
|
417 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
418 |
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
|
419 |
*} |
48481 | 420 |
options [document_graph] |
421 |
theories Example |
|
422 |
files "document/root.bib" "document/root.tex" |
|
423 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
424 |
session "HOL-Bali" in Bali = HOL + |
48481 | 425 |
options [document_graph] |
426 |
theories |
|
427 |
AxExample |
|
428 |
AxSound |
|
429 |
AxCompl |
|
430 |
Trans |
|
431 |
files "document/root.tex" |
|
432 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
433 |
session "HOL-IOA" in IOA = HOL + |
48481 | 434 |
description {* |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
435 |
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
|
436 |
Copyright 1994--1996 TU Muenchen |
48481 | 437 |
|
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
438 |
The meta theory of I/O-Automata in HOL. This formalization has been |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
439 |
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
|
440 |
proofs of two communication protocols which formerly have been here. |
48481 | 441 |
|
442 |
@inproceedings{Nipkow-Slind-IOA, |
|
443 |
author={Tobias Nipkow and Konrad Slind}, |
|
444 |
title={{I/O} Automata in {Isabelle/HOL}}, |
|
445 |
booktitle={Proc.\ TYPES Workshop 1994}, |
|
446 |
publisher=Springer, |
|
447 |
series=LNCS, |
|
448 |
note={To appear}} |
|
449 |
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz |
|
450 |
||
451 |
and |
|
452 |
||
453 |
@inproceedings{Mueller-Nipkow, |
|
454 |
author={Olaf M\"uller and Tobias Nipkow}, |
|
455 |
title={Combining Model Checking and Deduction for {I/O}-Automata}, |
|
456 |
booktitle={Proc.\ TACAS Workshop}, |
|
457 |
organization={Aarhus University, BRICS report}, |
|
458 |
year=1995} |
|
459 |
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz |
|
460 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
461 |
options [document = false] |
48481 | 462 |
theories Solve |
463 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
464 |
session "HOL-Lattice" in Lattice = HOL + |
48481 | 465 |
description {* |
466 |
Author: Markus Wenzel, TU Muenchen |
|
467 |
||
468 |
Basic theory of lattices and orders. |
|
469 |
*} |
|
470 |
theories CompleteLattice |
|
471 |
files "document/root.tex" |
|
472 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
473 |
session "HOL-ex" in ex = HOL + |
48481 | 474 |
description {* Miscellaneous examples for Higher-Order Logic. *} |
48679 | 475 |
options [timeout = 3600, condition = ISABELLE_POLYML] |
48481 | 476 |
theories [document = false] |
477 |
"~~/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
|
478 |
Code_Binary_Nat_examples |
48481 | 479 |
"~~/src/HOL/Library/FuncSet" |
480 |
Eval_Examples |
|
481 |
Normalization_by_Evaluation |
|
482 |
Hebrew |
|
483 |
Chinese |
|
484 |
Serbian |
|
485 |
"~~/src/HOL/Library/FinFun_Syntax" |
|
49985
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49932
diff
changeset
|
486 |
"~~/src/HOL/Library/Refute" |
48481 | 487 |
theories |
488 |
Iff_Oracle |
|
489 |
Coercion_Examples |
|
490 |
Numeral_Representation |
|
491 |
Higher_Order_Logic |
|
492 |
Abstract_NAT |
|
493 |
Guess |
|
494 |
Binary |
|
495 |
Fundefs |
|
496 |
Induction_Schema |
|
497 |
LocaleTest2 |
|
498 |
Records |
|
499 |
While_Combinator_Example |
|
500 |
MonoidGroup |
|
501 |
BinEx |
|
502 |
Hex_Bin_Examples |
|
503 |
Antiquote |
|
504 |
Multiquote |
|
505 |
PER |
|
506 |
NatSum |
|
507 |
ThreeDivides |
|
508 |
Intuitionistic |
|
509 |
CTL |
|
510 |
Arith_Examples |
|
511 |
BT |
|
512 |
Tree23 |
|
513 |
MergeSort |
|
514 |
Lagrange |
|
515 |
Groebner_Examples |
|
516 |
MT |
|
517 |
Unification |
|
518 |
Primrec |
|
519 |
Tarski |
|
520 |
Classical |
|
521 |
Set_Theory |
|
522 |
Meson_Test |
|
523 |
Termination |
|
524 |
Coherent |
|
525 |
PresburgerEx |
|
51093 | 526 |
Reflection_Examples |
48481 | 527 |
Sqrt |
528 |
Sqrt_Script |
|
529 |
Transfer_Ex |
|
530 |
Transfer_Int_Nat |
|
531 |
HarmonicSeries |
|
532 |
Refute_Examples |
|
533 |
Execute_Choice |
|
534 |
Summation |
|
535 |
Gauge_Integration |
|
536 |
Dedekind_Real |
|
537 |
Quicksort |
|
538 |
Birthday_Paradox |
|
539 |
List_to_Set_Comprehension_Examples |
|
540 |
Seq |
|
541 |
Simproc_Tests |
|
542 |
Executable_Relation |
|
543 |
FinFunPred |
|
544 |
Set_Comprehension_Pointfree_Tests |
|
545 |
Parallel_Example |
|
50138 | 546 |
IArray_Examples |
48481 | 547 |
theories SVC_Oracle |
48690 | 548 |
theories [condition = SVC_HOME] |
549 |
svc_test |
|
48481 | 550 |
theories [condition = ZCHAFF_HOME] |
551 |
(*requires zChaff (or some other reasonably fast SAT solver)*) |
|
552 |
Sudoku |
|
553 |
(* FIXME |
|
554 |
(*requires a proof-generating SAT solver (zChaff or MiniSAT)*) |
|
555 |
(*global side-effects ahead!*) |
|
556 |
try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *) |
|
557 |
*) |
|
558 |
files "document/root.bib" "document/root.tex" |
|
559 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
560 |
session "HOL-Isar_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
|
561 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
562 |
Miscellaneous Isabelle/Isar examples for Higher-Order Logic. |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
563 |
*} |
48481 | 564 |
theories [document = false] |
565 |
"~~/src/HOL/Library/Lattice_Syntax" |
|
566 |
"../Number_Theory/Primes" |
|
567 |
theories |
|
568 |
Basic_Logic |
|
569 |
Cantor |
|
570 |
Drinker |
|
571 |
Expr_Compiler |
|
572 |
Fibonacci |
|
573 |
Group |
|
574 |
Group_Context |
|
575 |
Group_Notepad |
|
576 |
Hoare_Ex |
|
577 |
Knaster_Tarski |
|
578 |
Mutilated_Checkerboard |
|
579 |
Nested_Datatype |
|
580 |
Peirce |
|
581 |
Puzzle |
|
582 |
Summation |
|
583 |
files |
|
584 |
"document/root.bib" |
|
585 |
"document/root.tex" |
|
586 |
"document/style.tex" |
|
587 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
588 |
session "HOL-SET_Protocol" in SET_Protocol = HOL + |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
589 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
590 |
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
|
591 |
*} |
48481 | 592 |
options [document_graph] |
593 |
theories [document = false] "~~/src/HOL/Library/Nat_Bijection" |
|
594 |
theories SET_Protocol |
|
595 |
files "document/root.tex" |
|
596 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
597 |
session "HOL-Matrix_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
|
598 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
599 |
Two-dimensional 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
|
600 |
*} |
48481 | 601 |
options [document_graph] |
602 |
theories Cplex |
|
603 |
files "document/root.tex" |
|
604 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
605 |
session "HOL-TLA" 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
|
606 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
607 |
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
|
608 |
*} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
609 |
options [document = false] |
48481 | 610 |
theories TLA |
611 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
612 |
session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
613 |
options [document = false] |
48481 | 614 |
theories Inc |
615 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
616 |
session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
617 |
options [document = false] |
48481 | 618 |
theories DBuffer |
619 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
620 |
session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
621 |
options [document = false] |
48481 | 622 |
theories MemoryImplementation |
623 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
624 |
session "HOL-TPTP" in TPTP = HOL + |
48481 | 625 |
description {* |
626 |
Author: Jasmin Blanchette, TU Muenchen |
|
627 |
Author: Nik Sultana, University of Cambridge |
|
628 |
Copyright 2011 |
|
629 |
||
630 |
TPTP-related extensions. |
|
631 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
632 |
options [document = false] |
48481 | 633 |
theories |
634 |
ATP_Theory_Export |
|
635 |
MaSh_Eval |
|
636 |
MaSh_Export |
|
637 |
TPTP_Interpret |
|
638 |
THF_Arith |
|
639 |
theories [proofs = 0] (* FIXME !? *) |
|
640 |
ATP_Problem_Import |
|
641 |
||
50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset
|
642 |
session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL + |
48481 | 643 |
options [document_graph] |
644 |
theories |
|
645 |
Multivariate_Analysis |
|
646 |
Determinants |
|
647 |
files |
|
648 |
"document/root.tex" |
|
649 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
650 |
session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" + |
48617 | 651 |
options [document_graph] |
48481 | 652 |
theories [document = false] |
653 |
"~~/src/HOL/Library/Countable" |
|
654 |
"~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits" |
|
655 |
"~~/src/HOL/Library/Permutation" |
|
656 |
theories |
|
657 |
Probability |
|
658 |
"ex/Dining_Cryptographers" |
|
659 |
"ex/Koepf_Duermuth_Countermeasure" |
|
660 |
files "document/root.tex" |
|
661 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
662 |
session "HOL-Nominal" (main) in Nominal = HOL + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
663 |
options [document = false] |
48481 | 664 |
theories Nominal |
665 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
666 |
session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" + |
48679 | 667 |
options [timeout = 3600, condition = ISABELLE_POLYML, document = false] |
48481 | 668 |
theories Nominal_Examples |
669 |
theories [quick_and_dirty] VC_Condition |
|
670 |
||
49310 | 671 |
session "HOL-Cardinals-Base" in Cardinals = HOL + |
48978 | 672 |
description {* Ordinals and Cardinals, Base Theories *} |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
673 |
options [document = false] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
674 |
theories Cardinal_Arithmetic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
675 |
|
49310 | 676 |
session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" + |
48978 | 677 |
description {* Ordinals and Cardinals, Full Theories *} |
49511
9f5bfef8bd82
created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents:
49510
diff
changeset
|
678 |
options [document = false] |
49439 | 679 |
theories Cardinals |
48984
f51d4a302962
do not hardwire document output options -- to be provided by the user;
wenzelm
parents:
48978
diff
changeset
|
680 |
files |
f51d4a302962
do not hardwire document output options -- to be provided by the user;
wenzelm
parents:
48978
diff
changeset
|
681 |
"document/intro.tex" |
f51d4a302962
do not hardwire document output options -- to be provided by the user;
wenzelm
parents:
48978
diff
changeset
|
682 |
"document/root.tex" |
f51d4a302962
do not hardwire document output options -- to be provided by the user;
wenzelm
parents:
48978
diff
changeset
|
683 |
"document/root.bib" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
684 |
|
49511
9f5bfef8bd82
created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents:
49510
diff
changeset
|
685 |
session "HOL-BNF-LFP" in BNF = "HOL-Cardinals-Base" + |
9f5bfef8bd82
created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents:
49510
diff
changeset
|
686 |
description {* Bounded Natural Functors for Datatypes *} |
9f5bfef8bd82
created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents:
49510
diff
changeset
|
687 |
options [document = false] |
9f5bfef8bd82
created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents:
49510
diff
changeset
|
688 |
theories BNF_LFP |
9f5bfef8bd82
created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
blanchet
parents:
49510
diff
changeset
|
689 |
|
49517
c473c8749cd1
changed base session for "HOL-BNF" for faster building in the typical case
blanchet
parents:
49511
diff
changeset
|
690 |
session "HOL-BNF" in BNF = "HOL-Cardinals" + |
49510
ba50d204095e
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
blanchet
parents:
49483
diff
changeset
|
691 |
description {* Bounded Natural Functors for (Co)datatypes *} |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
692 |
options [document = false] |
49510
ba50d204095e
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
blanchet
parents:
49483
diff
changeset
|
693 |
theories BNF |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
694 |
|
49510
ba50d204095e
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
blanchet
parents:
49483
diff
changeset
|
695 |
session "HOL-BNF-Examples" in "BNF/Examples" = "HOL-BNF" + |
ba50d204095e
renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
blanchet
parents:
49483
diff
changeset
|
696 |
description {* Examples for Bounded Natural Functors *} |
49932
9d3bc26485eb
back to parallel HOL-BNF-Examples, which seems to have suffered from Future.map on canceled persistent futures;
wenzelm
parents:
49903
diff
changeset
|
697 |
options [document = false] |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
698 |
theories |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
699 |
Lambda_Term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
700 |
Process |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
701 |
TreeFsetI |
49872 | 702 |
"Derivation_Trees/Gram_Lang" |
703 |
"Derivation_Trees/Parallel" |
|
50517 | 704 |
Koenig |
49693
393d7242adaf
thread the right local theory through + reenable parallel proofs for previously problematic theories
blanchet
parents:
49601
diff
changeset
|
705 |
theories [condition = ISABELLE_FULL_TEST] |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
706 |
Misc_Codata |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
707 |
Misc_Data |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
708 |
|
50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset
|
709 |
session "HOL-Word" (main) in Word = HOL + |
48481 | 710 |
options [document_graph] |
711 |
theories Word |
|
712 |
files "document/root.bib" "document/root.tex" |
|
713 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
714 |
session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
715 |
options [document = false] |
48481 | 716 |
theories WordExamples |
717 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
718 |
session "HOL-Statespace" in Statespace = HOL + |
48481 | 719 |
theories StateSpaceEx |
720 |
files "document/root.tex" |
|
721 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
722 |
session "HOL-NSA" in NSA = HOL + |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
723 |
description {* Nonstandard analysis. *} |
48481 | 724 |
options [document_graph] |
725 |
theories Hypercomplex |
|
726 |
files "document/root.tex" |
|
727 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
728 |
session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
729 |
options [document = false] |
48481 | 730 |
theories NSPrimes |
731 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
732 |
session "HOL-Mirabelle" in Mirabelle = HOL + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
733 |
options [document = false] |
48481 | 734 |
theories Mirabelle_Test |
48589
fb446a780d50
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
wenzelm
parents:
48588
diff
changeset
|
735 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
736 |
session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" + |
49448
8a232a4e3fd8
reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
wenzelm
parents:
49439
diff
changeset
|
737 |
options [document = false, timeout = 60] |
8a232a4e3fd8
reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
wenzelm
parents:
49439
diff
changeset
|
738 |
theories Ex |
48481 | 739 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
740 |
session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
741 |
options [document = false, quick_and_dirty] |
48481 | 742 |
theories |
743 |
SMT_Examples |
|
744 |
SMT_Word_Examples |
|
50666
6f48853f08d5
actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
blanchet
parents:
50665
diff
changeset
|
745 |
theories [condition = ISABELLE_FULL_TEST] |
6f48853f08d5
actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
blanchet
parents:
50665
diff
changeset
|
746 |
SMT_Tests |
48481 | 747 |
files |
748 |
"SMT_Examples.certs" |
|
50665 | 749 |
"SMT_Word_Examples.certs" |
48481 | 750 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
751 |
session "HOL-Boogie" in "Boogie" = "HOL-Word" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
752 |
options [document = false] |
48481 | 753 |
theories Boogie |
754 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
755 |
session "HOL-Boogie-Examples" in "Boogie/Examples" = "HOL-Boogie" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
756 |
options [document = false] |
48481 | 757 |
theories |
758 |
Boogie_Max_Stepwise |
|
759 |
Boogie_Max |
|
760 |
Boogie_Dijkstra |
|
761 |
VCC_Max |
|
762 |
files |
|
48493 | 763 |
"Boogie_Dijkstra.b2i" |
48481 | 764 |
"Boogie_Dijkstra.certs" |
48493 | 765 |
"Boogie_Max.b2i" |
48481 | 766 |
"Boogie_Max.certs" |
48493 | 767 |
"VCC_Max.b2i" |
48481 | 768 |
"VCC_Max.certs" |
769 |
||
50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset
|
770 |
session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
771 |
options [document = false] |
48481 | 772 |
theories SPARK |
773 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
774 |
session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
775 |
options [document = false] |
48481 | 776 |
theories |
777 |
"Gcd/Greatest_Common_Divisor" |
|
778 |
||
779 |
"Liseq/Longest_Increasing_Subsequence" |
|
780 |
||
781 |
"RIPEMD-160/F" |
|
782 |
"RIPEMD-160/Hash" |
|
783 |
"RIPEMD-160/K_L" |
|
784 |
"RIPEMD-160/K_R" |
|
785 |
"RIPEMD-160/R_L" |
|
786 |
"RIPEMD-160/Round" |
|
787 |
"RIPEMD-160/R_R" |
|
788 |
"RIPEMD-160/S_L" |
|
789 |
"RIPEMD-160/S_R" |
|
790 |
||
791 |
"Sqrt/Sqrt" |
|
792 |
files |
|
793 |
"Gcd/greatest_common_divisor/g_c_d.fdl" |
|
794 |
"Gcd/greatest_common_divisor/g_c_d.rls" |
|
795 |
"Gcd/greatest_common_divisor/g_c_d.siv" |
|
796 |
"Liseq/liseq/liseq_length.fdl" |
|
797 |
"Liseq/liseq/liseq_length.rls" |
|
798 |
"Liseq/liseq/liseq_length.siv" |
|
799 |
"RIPEMD-160/rmd/f.fdl" |
|
800 |
"RIPEMD-160/rmd/f.rls" |
|
801 |
"RIPEMD-160/rmd/f.siv" |
|
802 |
"RIPEMD-160/rmd/hash.fdl" |
|
803 |
"RIPEMD-160/rmd/hash.rls" |
|
804 |
"RIPEMD-160/rmd/hash.siv" |
|
805 |
"RIPEMD-160/rmd/k_l.fdl" |
|
806 |
"RIPEMD-160/rmd/k_l.rls" |
|
807 |
"RIPEMD-160/rmd/k_l.siv" |
|
808 |
"RIPEMD-160/rmd/k_r.fdl" |
|
809 |
"RIPEMD-160/rmd/k_r.rls" |
|
810 |
"RIPEMD-160/rmd/k_r.siv" |
|
811 |
"RIPEMD-160/rmd/r_l.fdl" |
|
812 |
"RIPEMD-160/rmd/r_l.rls" |
|
813 |
"RIPEMD-160/rmd/r_l.siv" |
|
814 |
"RIPEMD-160/rmd/round.fdl" |
|
815 |
"RIPEMD-160/rmd/round.rls" |
|
816 |
"RIPEMD-160/rmd/round.siv" |
|
817 |
"RIPEMD-160/rmd/r_r.fdl" |
|
818 |
"RIPEMD-160/rmd/r_r.rls" |
|
819 |
"RIPEMD-160/rmd/r_r.siv" |
|
820 |
"RIPEMD-160/rmd/s_l.fdl" |
|
821 |
"RIPEMD-160/rmd/s_l.rls" |
|
822 |
"RIPEMD-160/rmd/s_l.siv" |
|
823 |
"RIPEMD-160/rmd/s_r.fdl" |
|
824 |
"RIPEMD-160/rmd/s_r.rls" |
|
825 |
"RIPEMD-160/rmd/s_r.siv" |
|
826 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
827 |
session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" + |
48486 | 828 |
options [show_question_marks = false] |
48481 | 829 |
theories |
830 |
Example_Verification |
|
831 |
VC_Principles |
|
832 |
Reference |
|
833 |
Complex_Types |
|
834 |
files |
|
835 |
"complex_types_app/initialize.fdl" |
|
836 |
"complex_types_app/initialize.rls" |
|
837 |
"complex_types_app/initialize.siv" |
|
838 |
"document/complex_types.ads" |
|
839 |
"document/complex_types_app.adb" |
|
840 |
"document/complex_types_app.ads" |
|
841 |
"document/Gcd.adb" |
|
842 |
"document/Gcd.ads" |
|
843 |
"document/intro.tex" |
|
844 |
"document/loop_invariant.adb" |
|
845 |
"document/loop_invariant.ads" |
|
846 |
"document/root.bib" |
|
847 |
"document/root.tex" |
|
848 |
"document/Simple_Gcd.adb" |
|
849 |
"document/Simple_Gcd.ads" |
|
850 |
"loop_invariant/proc1.fdl" |
|
851 |
"loop_invariant/proc1.rls" |
|
852 |
"loop_invariant/proc1.siv" |
|
853 |
"loop_invariant/proc2.fdl" |
|
854 |
"loop_invariant/proc2.rls" |
|
855 |
"loop_invariant/proc2.siv" |
|
856 |
"simple_greatest_common_divisor/g_c_d.fdl" |
|
857 |
"simple_greatest_common_divisor/g_c_d.rls" |
|
858 |
"simple_greatest_common_divisor/g_c_d.siv" |
|
859 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
860 |
session "HOL-Mutabelle" in Mutabelle = HOL + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
861 |
options [document = false] |
48481 | 862 |
theories MutabelleExtra |
863 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
864 |
session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL + |
50179
978200ae8473
timeout in proper place (HOL-Quickcheck_Examples approx. 1min, HOL-Quickcheck_Benchmark approx. 1h);
wenzelm
parents:
50161
diff
changeset
|
865 |
options [document = false] |
48588 | 866 |
theories |
48690 | 867 |
Quickcheck_Examples |
868 |
(* FIXME |
|
869 |
Quickcheck_Lattice_Examples |
|
870 |
Completeness |
|
871 |
Quickcheck_Interfaces |
|
872 |
Hotel_Example *) |
|
48598 | 873 |
theories [condition = ISABELLE_GHC] |
874 |
Quickcheck_Narrowing_Examples |
|
48588 | 875 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
876 |
session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL + |
50571
b649e33e4821
HOL-Quickcheck_Benchmark works without timeout (NB: isatest imposes global timeout already);
wenzelm
parents:
50568
diff
changeset
|
877 |
theories [condition = ISABELLE_FULL_TEST, quick_and_dirty] |
50568
ee090b5712f3
reverting d466ebc27810 as the previous changeset should allow to run Find_Unused_Assms_Examples again
bulwahn
parents:
50517
diff
changeset
|
878 |
Find_Unused_Assms_Examples |
48618
1f7e068b4613
moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents:
48614
diff
changeset
|
879 |
Needham_Schroeder_No_Attacker_Example |
1f7e068b4613
moved another larger quickcheck example to Quickcheck_Benchmark
bulwahn
parents:
48614
diff
changeset
|
880 |
Needham_Schroeder_Guided_Attacker_Example |
48690 | 881 |
Needham_Schroeder_Unguided_Attacker_Example |
48481 | 882 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
883 |
session "HOL-Quotient_Examples" in Quotient_Examples = HOL + |
48481 | 884 |
description {* |
885 |
Author: Cezary Kaliszyk and Christian Urban |
|
886 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
887 |
options [document = false] |
48481 | 888 |
theories |
889 |
DList |
|
890 |
FSet |
|
891 |
Quotient_Int |
|
892 |
Quotient_Message |
|
893 |
Lift_FSet |
|
894 |
Lift_Set |
|
895 |
Lift_Fun |
|
896 |
Quotient_Rat |
|
897 |
Lift_DList |
|
898 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
899 |
session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
900 |
options [document = false] |
48690 | 901 |
theories |
48481 | 902 |
Examples |
903 |
Predicate_Compile_Tests |
|
48690 | 904 |
(* FIXME |
905 |
Predicate_Compile_Quickcheck_Examples -- should be added again soon (since 21-Oct-2010) *) |
|
48481 | 906 |
Specialisation_Examples |
48690 | 907 |
(* FIXME since 21-Jul-2011 |
908 |
Hotel_Example_Small_Generator |
|
909 |
IMP_1 |
|
910 |
IMP_2 |
|
911 |
IMP_3 |
|
912 |
IMP_4 *) |
|
913 |
theories [condition = "ISABELLE_SWIPL"] (* FIXME: *or* ISABELLE_YAP (??) *) |
|
914 |
Code_Prolog_Examples |
|
915 |
Context_Free_Grammar_Example |
|
916 |
Hotel_Example_Prolog |
|
917 |
Lambda_Example |
|
918 |
List_Examples |
|
919 |
theories [condition = "ISABELLE_SWIPL", quick_and_dirty] (* FIXME: *or* ISABELLE_YAP (??) *) |
|
920 |
Reg_Exp_Example |
|
48481 | 921 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
922 |
session HOLCF (main) in HOLCF = HOL + |
48338 | 923 |
description {* |
924 |
Author: Franz Regensburger |
|
925 |
Author: Brian Huffman |
|
926 |
||
927 |
HOLCF -- a semantic extension of HOL by the LCF logic. |
|
928 |
*} |
|
929 |
options [document_graph] |
|
48470
7483aa690b4f
clarified "document" again, eliminated redundant "no_document";
wenzelm
parents:
48458
diff
changeset
|
930 |
theories [document = false] |
48338 | 931 |
"~~/src/HOL/Library/Nat_Bijection" |
932 |
"~~/src/HOL/Library/Countable" |
|
48481 | 933 |
theories |
934 |
Plain_HOLCF |
|
935 |
Fixrec |
|
936 |
HOLCF |
|
937 |
files "document/root.tex" |
|
938 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
939 |
session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF + |
48481 | 940 |
theories |
941 |
Domain_ex |
|
942 |
Fixrec_ex |
|
943 |
New_Domain |
|
944 |
files "document/root.tex" |
|
945 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
946 |
session "HOLCF-Library" in "HOLCF/Library" = HOLCF + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
947 |
options [document = false] |
48481 | 948 |
theories HOLCF_Library |
949 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
950 |
session "HOLCF-IMP" 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
|
951 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
952 |
IMP -- A WHILE-language and its Semantics. |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
953 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
954 |
This is the HOLCF-based denotational semantics of a simple WHILE-language. |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
955 |
*} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
956 |
options [document = false] |
48481 | 957 |
theories HoareEx |
48338 | 958 |
files "document/root.tex" |
959 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
960 |
session "HOLCF-ex" in "HOLCF/ex" = HOLCF + |
48481 | 961 |
description {* Misc HOLCF examples *} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
962 |
options [document = false] |
48481 | 963 |
theories |
964 |
Dnat |
|
965 |
Dagstuhl |
|
966 |
Focus_ex |
|
967 |
Fix2 |
|
968 |
Hoare |
|
969 |
Concurrency_Monad |
|
970 |
Loop |
|
971 |
Powerdomain_ex |
|
972 |
Domain_Proofs |
|
973 |
Letrec |
|
974 |
Pattern_Match |
|
975 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
976 |
session "HOLCF-FOCUS" 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
|
977 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
978 |
FOCUS: a theory of stream-processing functions Isabelle/HOLCF. |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
979 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
980 |
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
|
981 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
982 |
"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
|
983 |
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
|
984 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
985 |
"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
|
986 |
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
|
987 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
988 |
"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
|
989 |
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
|
990 |
*} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
991 |
options [document = false] |
48481 | 992 |
theories |
993 |
Fstreams |
|
994 |
FOCUS |
|
995 |
Buffer_adm |
|
996 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
997 |
session IOA in "HOLCF/IOA" = HOLCF + |
48481 | 998 |
description {* |
999 |
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
|
1000 |
Copyright 1997 TU München |
48481 | 1001 |
|
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1002 |
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
|
1003 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1004 |
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
|
1005 |
abstraction theory. Everything is based upon a domain-theoretic model of |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1006 |
finite and infinite sequences. |
48481 | 1007 |
*} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1008 |
options [document = false] |
48481 | 1009 |
theories "meta_theory/Abstraction" |
1010 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1011 |
session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA + |
48481 | 1012 |
description {* |
1013 |
Author: Olaf Mueller |
|
1014 |
||
1015 |
The Alternating Bit Protocol performed in I/O-Automata. |
|
1016 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1017 |
options [document = false] |
48481 | 1018 |
theories Correctness |
1019 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1020 |
session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA + |
48481 | 1021 |
description {* |
1022 |
Author: Tobias Nipkow & Konrad Slind |
|
1023 |
||
1024 |
A network transmission protocol, performed in the |
|
1025 |
I/O automata formalization by Olaf Mueller. |
|
1026 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1027 |
options [document = false] |
48481 | 1028 |
theories Correctness |
1029 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1030 |
session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA + |
48481 | 1031 |
description {* |
1032 |
Author: Olaf Mueller |
|
1033 |
||
1034 |
Memory storage case study. |
|
1035 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1036 |
options [document = false] |
48481 | 1037 |
theories Correctness |
1038 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1039 |
session "IOA-ex" in "HOLCF/IOA/ex" = IOA + |
48481 | 1040 |
description {* |
1041 |
Author: Olaf Mueller |
|
1042 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1043 |
options [document = false] |
48481 | 1044 |
theories |
1045 |
TrivEx |
|
1046 |
TrivEx2 |
|
1047 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1048 |
session "HOL-Datatype_Benchmark" in Datatype_Benchmark = HOL + |
48481 | 1049 |
description {* Some rather large datatype examples (from John Harrison). *} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1050 |
options [document = false] |
48635 | 1051 |
theories [condition = ISABELLE_FULL_TEST, timing] |
48481 | 1052 |
Brackin |
1053 |
Instructions |
|
1054 |
SML |
|
1055 |
Verilog |
|
1056 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1057 |
session "HOL-Record_Benchmark" in Record_Benchmark = HOL + |
48481 | 1058 |
description {* Some benchmark on large record. *} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1059 |
options [document = false] |
48635 | 1060 |
theories [condition = ISABELLE_FULL_TEST, timing] |
48481 | 1061 |
Record_Benchmark |
1062 |