author | haftmann |
Tue, 03 Mar 2020 19:26:24 +0000 | |
changeset 71518 | bae868febc53 |
parent 71494 | cbe0b6b0bed8 |
child 71766 | 1249b998e377 |
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 + |
69319 | 4 |
description " |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
5 |
Classical Higher-order Logic. |
69319 | 6 |
" |
70678
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents:
70675
diff
changeset
|
7 |
options [strict_facts] |
70853 | 8 |
sessions Tools |
70796
2739631ac368
discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;
wenzelm
parents:
70781
diff
changeset
|
9 |
theories |
65374 | 10 |
Main (global) |
11 |
Complex_Main (global) |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
12 |
document_files |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
13 |
"root.bib" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
14 |
"root.tex" |
48338 | 15 |
|
70669 | 16 |
session "HOL-Proofs" (timing) in Proofs = Pure + |
69319 | 17 |
description " |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
18 |
HOL-Main with explicit proof terms. |
69319 | 19 |
" |
70398 | 20 |
options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500] |
65543 | 21 |
sessions |
22 |
"HOL-Library" |
|
65530
09c00a304c00
include imports that morally belong to Main and are used in HOL-Proofs applications;
wenzelm
parents:
65509
diff
changeset
|
23 |
theories |
67319
07176d5b81d5
moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
blanchet
parents:
67278
diff
changeset
|
24 |
"HOL-Library.Realizers" |
48338 | 25 |
|
63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset
|
26 |
session "HOL-Library" (main timing) in Library = HOL + |
69319 | 27 |
description " |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
28 |
Classical Higher-order Logic -- batteries included. |
69319 | 29 |
" |
48481 | 30 |
theories |
31 |
Library |
|
64588 | 32 |
(*conflicting type class instantiations and dependent applications*) |
33 |
Finite_Lattice |
|
68312 | 34 |
List_Lexorder |
63763
0f61ea70d384
clarified session: use all theories in directory HOL/Library;
wenzelm
parents:
63731
diff
changeset
|
35 |
Prefix_Order |
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51093
diff
changeset
|
36 |
Product_Lexorder |
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51093
diff
changeset
|
37 |
Product_Order |
65956
639eb3617a86
reorganised material on sublists
eberlm <eberlm@in.tum.de>
parents:
65678
diff
changeset
|
38 |
Subseq_Order |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
67319
diff
changeset
|
39 |
(*conflicting syntax*) |
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
67319
diff
changeset
|
40 |
Datatype_Records |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
41 |
(*data refinements and dependent applications*) |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
42 |
AList_Mapping |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
43 |
Code_Binary_Nat |
55447 | 44 |
Code_Prolog |
48481 | 45 |
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
|
46 |
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
|
47 |
DAList |
54429
be1bc181bcde
explicit inclusion of data refinement theory into HOL-Library session
haftmann
parents:
54193
diff
changeset
|
48 |
DAList_Multiset |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
49 |
RBT_Mapping |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
50 |
RBT_Set |
66015
70643edecb7a
specific output setup is not supposed to intrude regular import theory
haftmann
parents:
65956
diff
changeset
|
51 |
(*printing modifications*) |
70643edecb7a
specific output setup is not supposed to intrude regular import theory
haftmann
parents:
65956
diff
changeset
|
52 |
OptionalSugar |
64588 | 53 |
(*prototypic tools*) |
54 |
Predicate_Compile_Quickcheck |
|
71518
bae868febc53
library theory for extractions of equations x = t into premises
haftmann
parents:
71494
diff
changeset
|
55 |
Quantified_Premise_Simproc |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
56 |
(*legacy tools*) |
58372
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents:
58371
diff
changeset
|
57 |
Old_Datatype |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
58 |
Old_Recdef |
67319
07176d5b81d5
moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
blanchet
parents:
67278
diff
changeset
|
59 |
Realizers |
64588 | 60 |
Refute |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
61 |
document_files "root.bib" "root.tex" |
48481 | 62 |
|
66932
149025fecca0
reduced heap hierarchy, for potentially improved performance;
wenzelm
parents:
66842
diff
changeset
|
63 |
session "HOL-Analysis" (main timing) in Analysis = HOL + |
68617 | 64 |
options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", |
67152
8021ea06aad8
just one session for bulky HOL-Analysis documents;
wenzelm
parents:
67122
diff
changeset
|
65 |
document_variants = "document:manual=-proof,-ML,-unimportant"] |
66932
149025fecca0
reduced heap hierarchy, for potentially improved performance;
wenzelm
parents:
66842
diff
changeset
|
66 |
sessions |
67152
8021ea06aad8
just one session for bulky HOL-Analysis documents;
wenzelm
parents:
67122
diff
changeset
|
67 |
"HOL-Library" |
66932
149025fecca0
reduced heap hierarchy, for potentially improved performance;
wenzelm
parents:
66842
diff
changeset
|
68 |
"HOL-Computational_Algebra" |
70781
a37e2ea96c6d
just one dump_checkpoint Main -- potentially more robust;
wenzelm
parents:
70678
diff
changeset
|
69 |
theories |
65462
db1827610513
less global theories -- conflict with AFP entries;
wenzelm
parents:
65456
diff
changeset
|
70 |
Analysis |
65375 | 71 |
document_files |
72 |
"root.tex" |
|
69518 | 73 |
"root.bib" |
65375 | 74 |
|
71189
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset
|
75 |
session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" + |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset
|
76 |
options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset
|
77 |
document_variants = "document:manual=-proof,-ML,-unimportant"] |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset
|
78 |
theories |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset
|
79 |
Complex_Analysis |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset
|
80 |
document_files |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset
|
81 |
"root.tex" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset
|
82 |
"root.bib" |
954ee5acaae0
Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
71042
diff
changeset
|
83 |
|
65375 | 84 |
session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" + |
85 |
theories |
|
86 |
Approximations |
|
70956
860198428664
added examples for "metric" method, by Maximilian Schäffeler
immler
parents:
70853
diff
changeset
|
87 |
Metric_Arith_Examples |
65375 | 88 |
|
70151 | 89 |
session "HOL-Homology" (timing) in Homology = "HOL-Analysis" + |
70089
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset
|
90 |
options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", |
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset
|
91 |
document_variants = "document:manual=-proof,-ML,-unimportant"] |
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset
|
92 |
sessions |
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset
|
93 |
"HOL-Algebra" |
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset
|
94 |
theories |
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset
|
95 |
Homology |
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset
|
96 |
document_files |
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset
|
97 |
"root.tex" |
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
paulson <lp15@cam.ac.uk>
parents:
70086
diff
changeset
|
98 |
|
67100 | 99 |
session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" + |
65417 | 100 |
theories |
101 |
Computational_Algebra |
|
102 |
(*conflicting type class instantiations and dependent applications*) |
|
103 |
Field_as_Ring |
|
104 |
||
68630 | 105 |
session "HOL-Real_Asymp" in Real_Asymp = HOL + |
106 |
sessions |
|
107 |
"HOL-Decision_Procs" |
|
108 |
theories |
|
109 |
Real_Asymp |
|
110 |
Real_Asymp_Approx |
|
68677 | 111 |
Real_Asymp_Examples |
112 |
||
113 |
session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" + |
|
114 |
theories |
|
115 |
Real_Asymp_Doc |
|
116 |
document_files (in "~~/src/Doc") |
|
117 |
"iman.sty" |
|
118 |
"extra.sty" |
|
119 |
"isar.sty" |
|
120 |
document_files |
|
121 |
"root.tex" |
|
122 |
"style.sty" |
|
68630 | 123 |
|
65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset
|
124 |
session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" + |
69319 | 125 |
description " |
48481 | 126 |
Author: Gertrud Bauer, TU Munich |
127 |
||
128 |
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
|
129 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
130 |
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
|
131 |
following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach |
55018
2a526bd279ed
moved 'Zorn' into 'Main', since it's a BNF dependency
blanchet
parents:
54961
diff
changeset
|
132 |
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
|
133 |
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
|
134 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
135 |
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
|
136 |
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
|
137 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
138 |
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
|
139 |
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
|
140 |
continous linearform on the whole vectorspace. |
69319 | 141 |
" |
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
142 |
sessions |
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
143 |
"HOL-Analysis" |
65543 | 144 |
theories |
145 |
Hahn_Banach |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
146 |
document_files "root.bib" "root.tex" |
48481 | 147 |
|
65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset
|
148 |
session "HOL-Induct" in Induct = "HOL-Library" + |
69319 | 149 |
description " |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
150 |
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
|
151 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
152 |
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
|
153 |
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
|
154 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
155 |
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
|
156 |
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
|
157 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
158 |
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
|
159 |
(see |
58372
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents:
58371
diff
changeset
|
160 |
http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz). |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
161 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
162 |
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
|
163 |
mutually recursive relations. |
69319 | 164 |
" |
48481 | 165 |
theories [quick_and_dirty] |
166 |
Common_Patterns |
|
167 |
theories |
|
61935 | 168 |
Nested_Datatype |
48481 | 169 |
QuoDataType |
170 |
QuoNestedDataType |
|
171 |
Term |
|
172 |
SList |
|
173 |
ABexp |
|
65562
f9753d949afc
renamed theory to avoid conflict with loaded theory "Tree" from HOL-Library;
wenzelm
parents:
65552
diff
changeset
|
174 |
Infinitely_Branching_Tree |
48481 | 175 |
Ordinals |
176 |
Sigma_Algebra |
|
177 |
Comb |
|
178 |
PropLog |
|
179 |
Com |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
180 |
document_files "root.tex" |
48481 | 181 |
|
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
182 |
session "HOL-IMP" (timing) in IMP = "HOL-Library" + |
59446 | 183 |
options [document_variants = document] |
48481 | 184 |
theories |
185 |
BExp |
|
186 |
ASM |
|
50050 | 187 |
Finite_Reachable |
52394 | 188 |
Denotational |
52400 | 189 |
Compiler2 |
48481 | 190 |
Poly_Types |
191 |
Sec_Typing |
|
192 |
Sec_TypingT |
|
52726 | 193 |
Def_Init_Big |
194 |
Def_Init_Small |
|
195 |
Fold |
|
48481 | 196 |
Live |
197 |
Live_True |
|
198 |
Hoare_Examples |
|
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
63537
diff
changeset
|
199 |
Hoare_Sound_Complete |
52269 | 200 |
VCG |
52282 | 201 |
Hoare_Total |
63538
d7b5e2a222c2
added new vcg based on existentially quantified while-rule
nipkow
parents:
63537
diff
changeset
|
202 |
VCG_Total_EX |
67019
7a3724078363
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
nipkow
parents:
66992
diff
changeset
|
203 |
VCG_Total_EX2 |
48481 | 204 |
Collecting1 |
48765
fb1ed5230abc
special code with lists no longer necessary, use sets
nipkow
parents:
48738
diff
changeset
|
205 |
Collecting_Examples |
48481 | 206 |
Abs_Int_Tests |
207 |
Abs_Int1_parity |
|
208 |
Abs_Int1_const |
|
209 |
Abs_Int3 |
|
210 |
Procs_Dyn_Vars_Dyn |
|
211 |
Procs_Stat_Vars_Dyn |
|
212 |
Procs_Stat_Vars_Stat |
|
213 |
C_like |
|
214 |
OO |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
215 |
document_files "root.bib" "root.tex" |
48481 | 216 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
217 |
session "HOL-IMPP" in IMPP = HOL + |
69272 | 218 |
description \<open> |
48481 | 219 |
Author: David von Oheimb |
220 |
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
|
221 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
222 |
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
|
223 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
224 |
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
|
225 |
procedures. For documentation see "Hoare Logic for Mutual Recursion and |
68649 | 226 |
Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). |
69319 | 227 |
\<close> |
48481 | 228 |
theories EvenOdd |
229 |
||
63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset
|
230 |
session "HOL-Data_Structures" (timing) in Data_Structures = HOL + |
61203 | 231 |
options [document_variants = document] |
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
232 |
sessions |
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
233 |
"HOL-Number_Theory" |
61203 | 234 |
theories [document = false] |
65538 | 235 |
Less_False |
61203 | 236 |
theories |
66543 | 237 |
Sorting |
63829 | 238 |
Balance |
61203 | 239 |
Tree_Map |
71414 | 240 |
Interval_Tree |
61232 | 241 |
AVL_Map |
71352 | 242 |
RBT_Set2 |
61224 | 243 |
RBT_Map |
61469
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
61368
diff
changeset
|
244 |
Tree23_Map |
61514 | 245 |
Tree234_Map |
61789 | 246 |
Brother12_Map |
62130 | 247 |
AA_Map |
68261 | 248 |
Set2_Join_RBT |
69145 | 249 |
Array_Braun |
70250 | 250 |
Trie_Fun |
251 |
Trie_Map |
|
252 |
Tries_Binary |
|
62706 | 253 |
Leftist_Heap |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
66270
diff
changeset
|
254 |
Binomial_Heap |
61224 | 255 |
document_files "root.tex" "root.bib" |
61203 | 256 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
257 |
session "HOL-Import" in Import = HOL + |
48481 | 258 |
theories HOL_Light_Maps |
259 |
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import |
|
260 |
||
67100 | 261 |
session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" + |
69319 | 262 |
description " |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset
|
263 |
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
|
264 |
Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity. |
69319 | 265 |
" |
65543 | 266 |
sessions |
267 |
"HOL-Algebra" |
|
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset
|
268 |
theories |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset
|
269 |
Number_Theory |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
270 |
document_files |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
271 |
"root.tex" |
48481 | 272 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
273 |
session "HOL-Hoare" in Hoare = HOL + |
69319 | 274 |
description " |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
275 |
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
|
276 |
automatically from pre/post conditions and loop invariants). |
69319 | 277 |
" |
48481 | 278 |
theories Hoare |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
279 |
document_files "root.bib" "root.tex" |
48481 | 280 |
|
63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset
|
281 |
session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL + |
69319 | 282 |
description " |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
283 |
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
|
284 |
(verification conditions are generated automatically). |
69319 | 285 |
" |
48481 | 286 |
theories Hoare_Parallel |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
287 |
document_files "root.bib" "root.tex" |
48481 | 288 |
|
65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset
|
289 |
session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" + |
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
290 |
sessions |
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
291 |
"HOL-Data_Structures" |
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
292 |
"HOL-ex" |
51422
821a70e29e0b
proper formatting, to facilitate line-based diff;
wenzelm
parents:
51421
diff
changeset
|
293 |
theories |
821a70e29e0b
proper formatting, to facilitate line-based diff;
wenzelm
parents:
51421
diff
changeset
|
294 |
Generate |
821a70e29e0b
proper formatting, to facilitate line-based diff;
wenzelm
parents:
51421
diff
changeset
|
295 |
Generate_Binary_Nat |
821a70e29e0b
proper formatting, to facilitate line-based diff;
wenzelm
parents:
51421
diff
changeset
|
296 |
Generate_Target_Nat |
821a70e29e0b
proper formatting, to facilitate line-based diff;
wenzelm
parents:
51421
diff
changeset
|
297 |
Generate_Efficient_Datastructures |
68155 | 298 |
Code_Lazy_Test |
64582
3d20ded18f14
unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
wenzelm
parents:
64569
diff
changeset
|
299 |
Code_Test_PolyML |
3d20ded18f14
unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
wenzelm
parents:
64569
diff
changeset
|
300 |
Code_Test_Scala |
66842 | 301 |
theories [condition = ISABELLE_GHC] |
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset
|
302 |
Code_Test_GHC |
66842 | 303 |
theories [condition = ISABELLE_MLTON] |
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset
|
304 |
Code_Test_MLton |
69926
110fff287217
access OCaml tools and libraries via ISABELLE_OCAMLFIND;
wenzelm
parents:
69716
diff
changeset
|
305 |
theories [condition = ISABELLE_OCAMLFIND] |
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset
|
306 |
Code_Test_OCaml |
66842 | 307 |
theories [condition = ISABELLE_SMLNJ] |
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset
|
308 |
Code_Test_SMLNJ |
48481 | 309 |
|
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
310 |
session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" + |
69319 | 311 |
description " |
48481 | 312 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
313 |
Author: Jasmin Blanchette, TU Muenchen |
|
314 |
||
315 |
Testing Metis and Sledgehammer. |
|
69319 | 316 |
" |
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
317 |
sessions |
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
318 |
"HOL-Decision_Procs" |
48481 | 319 |
theories |
320 |
Abstraction |
|
321 |
Big_O |
|
322 |
Binary_Tree |
|
323 |
Clausification |
|
324 |
Message |
|
325 |
Proxies |
|
326 |
Tarski |
|
327 |
Trans_Closure |
|
328 |
Sets |
|
329 |
||
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
330 |
session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" + |
69319 | 331 |
description " |
48481 | 332 |
Author: Jasmin Blanchette, TU Muenchen |
333 |
Copyright 2009 |
|
69319 | 334 |
" |
48481 | 335 |
theories [quick_and_dirty] Nitpick_Examples |
336 |
||
65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset
|
337 |
session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" + |
69319 | 338 |
description " |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68522
diff
changeset
|
339 |
Author: Clemens Ballarin, started 24 September 1999, and many others |
48481 | 340 |
|
341 |
The Isabelle Algebraic Library. |
|
69319 | 342 |
" |
70660
373d95cf1b98
proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
wenzelm
parents:
70646
diff
changeset
|
343 |
sessions |
373d95cf1b98
proper session-qualifier imports (amending "fixes" from adaa0a6ea4fe);
wenzelm
parents:
70646
diff
changeset
|
344 |
"HOL-Cardinals" |
48481 | 345 |
theories |
65099
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
65050
diff
changeset
|
346 |
(* Orders and Lattices *) |
30d0b2f1df76
Knaster-Tarski fixed point theorem and Galois Connections.
ballarin
parents:
65050
diff
changeset
|
347 |
Galois_Connection (* Knaster-Tarski theorem and Galois connections *) |
48481 | 348 |
(* Groups *) |
349 |
FiniteProduct (* Product operator for commutative groups *) |
|
350 |
Sylow (* Sylow's theorem *) |
|
351 |
Bij (* Automorphism Groups *) |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65382
diff
changeset
|
352 |
Multiplicative_Group |
68443
43055b016688
New material from Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68312
diff
changeset
|
353 |
Zassenhaus (* The Zassenhaus lemma *) |
48481 | 354 |
(* Rings *) |
355 |
Divisibility (* Rings *) |
|
356 |
IntRing (* Ideals and residue classes *) |
|
357 |
UnivPoly (* Polynomials *) |
|
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
68522
diff
changeset
|
358 |
(* Main theory *) |
70078 | 359 |
Algebra |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
360 |
document_files "root.bib" "root.tex" |
48481 | 361 |
|
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
362 |
session "HOL-Auth" (timing) in Auth = "HOL-Library" + |
69319 | 363 |
description " |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
364 |
A new approach to verifying authentication protocols. |
69319 | 365 |
" |
70675 | 366 |
directories "Smartcard" "Guard" |
48481 | 367 |
theories |
368 |
Auth_Shared |
|
369 |
Auth_Public |
|
370 |
"Smartcard/Auth_Smartcard" |
|
371 |
"Guard/Auth_Guard_Shared" |
|
372 |
"Guard/Auth_Guard_Public" |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
373 |
document_files "root.tex" |
48481 | 374 |
|
63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset
|
375 |
session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" + |
69319 | 376 |
description " |
48481 | 377 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
378 |
Copyright 1998 University of Cambridge |
|
379 |
||
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
380 |
Verifying security protocols using Chandy and Misra's UNITY formalism. |
69319 | 381 |
" |
70675 | 382 |
directories "Simple" "Comp" |
48481 | 383 |
theories |
384 |
(*Basic meta-theory*) |
|
65538 | 385 |
UNITY_Main |
48481 | 386 |
|
387 |
(*Simple examples: no composition*) |
|
388 |
"Simple/Deadlock" |
|
389 |
"Simple/Common" |
|
390 |
"Simple/Network" |
|
391 |
"Simple/Token" |
|
392 |
"Simple/Channel" |
|
393 |
"Simple/Lift" |
|
394 |
"Simple/Mutex" |
|
395 |
"Simple/Reach" |
|
396 |
"Simple/Reachability" |
|
397 |
||
398 |
(*Verifying security protocols using UNITY*) |
|
399 |
"Simple/NSP_Bad" |
|
400 |
||
401 |
(*Example of composition*) |
|
402 |
"Comp/Handshake" |
|
403 |
||
404 |
(*Universal properties examples*) |
|
405 |
"Comp/Counter" |
|
406 |
"Comp/Counterc" |
|
407 |
"Comp/Priority" |
|
408 |
||
409 |
"Comp/TimerArray" |
|
410 |
"Comp/Progress" |
|
411 |
||
412 |
"Comp/Alloc" |
|
413 |
"Comp/AllocImpl" |
|
414 |
"Comp/Client" |
|
415 |
||
416 |
(*obsolete*) |
|
65538 | 417 |
ELT |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
418 |
document_files "root.tex" |
48481 | 419 |
|
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
420 |
session "HOL-Unix" in Unix = "HOL-Library" + |
48481 | 421 |
options [print_mode = "no_brackets,no_type_brackets"] |
422 |
theories Unix |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
423 |
document_files "root.bib" "root.tex" |
48481 | 424 |
|
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
425 |
session "HOL-ZF" in ZF = "HOL-Library" + |
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
426 |
theories |
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
427 |
MainZF |
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
428 |
Games |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
429 |
document_files "root.tex" |
48481 | 430 |
|
66986 | 431 |
session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" + |
70678
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents:
70675
diff
changeset
|
432 |
options [print_mode = "iff,no_brackets"] |
70675 | 433 |
directories "ex" |
48481 | 434 |
theories Imperative_HOL_ex |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
435 |
document_files "root.bib" "root.tex" |
48481 | 436 |
|
65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset
|
437 |
session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" + |
69319 | 438 |
description " |
51544 | 439 |
Various decision procedures, typically involving reflection. |
69319 | 440 |
" |
70675 | 441 |
directories "ex" |
65543 | 442 |
theories |
443 |
Decision_Procs |
|
48481 | 444 |
|
63000
d0dfdd413a7f
remove "slow" session tags
Lars Hupel <lars.hupel@mytum.de>
parents:
62999
diff
changeset
|
445 |
session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + |
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
446 |
sessions |
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
447 |
"HOL-Isar_Examples" |
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
52400
diff
changeset
|
448 |
theories |
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
52400
diff
changeset
|
449 |
Hilbert_Classical |
62363
7b5468422352
moved examples to avoid dependency on bulky HOL-Proofs session, e.g. relevant for "isabelle makedist";
wenzelm
parents:
62357
diff
changeset
|
450 |
Proof_Terms |
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
52400
diff
changeset
|
451 |
XML_Data |
48481 | 452 |
|
63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset
|
453 |
session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" + |
69319 | 454 |
description " |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
455 |
Examples for program extraction in Higher-Order Logic. |
69319 | 456 |
" |
70398 | 457 |
options [quick_and_dirty = false] |
65543 | 458 |
sessions |
459 |
"HOL-Computational_Algebra" |
|
48481 | 460 |
theories |
461 |
Greatest_Common_Divisor |
|
462 |
Warshall |
|
463 |
Higman_Extraction |
|
464 |
Pigeonhole |
|
465 |
Euclid |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
466 |
document_files "root.bib" "root.tex" |
48481 | 467 |
|
63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset
|
468 |
session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" + |
69272 | 469 |
description \<open> |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
470 |
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
|
471 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
472 |
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
|
473 |
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
|
474 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
475 |
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
|
476 |
theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). |
69319 | 477 |
\<close> |
70398 | 478 |
options [print_mode = "no_brackets", quick_and_dirty = false] |
65543 | 479 |
sessions |
480 |
"HOL-Library" |
|
48481 | 481 |
theories |
482 |
Eta |
|
483 |
StrongNorm |
|
484 |
Standardization |
|
485 |
WeakNorm |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
486 |
document_files "root.bib" "root.tex" |
48481 | 487 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
488 |
session "HOL-Prolog" in Prolog = HOL + |
69319 | 489 |
description " |
48481 | 490 |
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
|
491 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
492 |
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
|
493 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
494 |
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
|
495 |
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
|
496 |
a little functional language and its type system. |
69319 | 497 |
" |
48481 | 498 |
theories Test Type |
499 |
||
65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset
|
500 |
session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" + |
69319 | 501 |
description " |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
502 |
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
|
503 |
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
|
504 |
bytecode verifier, including proofs of type-safety. |
69319 | 505 |
" |
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
506 |
sessions |
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
507 |
"HOL-Eisbach" |
70678
36c8c32346cb
clarified syntax: 'directories' and 'theories' belong together;
wenzelm
parents:
70675
diff
changeset
|
508 |
directories "BV" "Comp" "DFA" "J" "JVM" |
59446 | 509 |
theories |
510 |
MicroJava |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
511 |
document_files |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
512 |
"introduction.tex" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
513 |
"root.bib" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
514 |
"root.tex" |
48481 | 515 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
516 |
session "HOL-NanoJava" in NanoJava = HOL + |
69319 | 517 |
description " |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
518 |
Hoare Logic for a tiny fragment of Java. |
69319 | 519 |
" |
48481 | 520 |
theories Example |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
521 |
document_files "root.bib" "root.tex" |
48481 | 522 |
|
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
523 |
session "HOL-Bali" (timing) in Bali = "HOL-Library" + |
48481 | 524 |
theories |
525 |
AxExample |
|
526 |
AxSound |
|
527 |
AxCompl |
|
528 |
Trans |
|
60751 | 529 |
TypeSafe |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
530 |
document_files "root.tex" |
48481 | 531 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
532 |
session "HOL-IOA" in IOA = HOL + |
69272 | 533 |
description \<open> |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
534 |
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
|
535 |
Copyright 1994--1996 TU Muenchen |
48481 | 536 |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55370
diff
changeset
|
537 |
The meta-theory of I/O-Automata 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
|
538 |
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
|
539 |
proofs of two communication protocols which formerly have been here. |
48481 | 540 |
|
541 |
@inproceedings{Nipkow-Slind-IOA, |
|
542 |
author={Tobias Nipkow and Konrad Slind}, |
|
543 |
title={{I/O} Automata in {Isabelle/HOL}}, |
|
544 |
booktitle={Proc.\ TYPES Workshop 1994}, |
|
545 |
publisher=Springer, |
|
546 |
series=LNCS, |
|
547 |
note={To appear}} |
|
548 |
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz |
|
549 |
||
550 |
and |
|
551 |
||
552 |
@inproceedings{Mueller-Nipkow, |
|
553 |
author={Olaf M\"uller and Tobias Nipkow}, |
|
554 |
title={Combining Model Checking and Deduction for {I/O}-Automata}, |
|
555 |
booktitle={Proc.\ TACAS Workshop}, |
|
556 |
organization={Aarhus University, BRICS report}, |
|
557 |
year=1995} |
|
558 |
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz |
|
69319 | 559 |
\<close> |
48481 | 560 |
theories Solve |
561 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
562 |
session "HOL-Lattice" in Lattice = HOL + |
69319 | 563 |
description " |
48481 | 564 |
Author: Markus Wenzel, TU Muenchen |
565 |
||
566 |
Basic theory of lattices and orders. |
|
69319 | 567 |
" |
48481 | 568 |
theories CompleteLattice |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
569 |
document_files "root.tex" |
48481 | 570 |
|
66752 | 571 |
session "HOL-ex" (timing) in ex = "HOL-Number_Theory" + |
69319 | 572 |
description " |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
573 |
Miscellaneous examples for Higher-Order Logic. |
69319 | 574 |
" |
65548 | 575 |
theories |
57507 | 576 |
Adhoc_Overloading_Examples |
48481 | 577 |
Antiquote |
65549 | 578 |
Argo_Examples |
579 |
Arith_Examples |
|
580 |
Ballot |
|
581 |
BinEx |
|
582 |
Birthday_Paradox |
|
67909
f55b07f4d1ee
proof of concept for algebraically founded bit lists
haftmann
parents:
67612
diff
changeset
|
583 |
Bit_Lists |
65549 | 584 |
Bubblesort |
585 |
CTL |
|
586 |
Cartouche_Examples |
|
65563 | 587 |
Case_Product |
65549 | 588 |
Chinese |
589 |
Classical |
|
590 |
Code_Binary_Nat_examples |
|
68639 | 591 |
Code_Lazy_Demo |
65549 | 592 |
Code_Timing |
593 |
Coercion_Examples |
|
594 |
Coherent |
|
595 |
Commands |
|
596 |
Computations |
|
67224 | 597 |
Conditional_Parametricity_Examples |
59190
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
59162
diff
changeset
|
598 |
Cubic_Quartic |
67611
7929240e44d4
records based on datatypes/BNF infrastructure
Lars Hupel <lars.hupel@mytum.de>
parents:
67319
diff
changeset
|
599 |
Datatype_Record_Examples |
65549 | 600 |
Dedekind_Real |
601 |
Erdoes_Szekeres |
|
602 |
Eval_Examples |
|
603 |
Executable_Relation |
|
604 |
Execute_Choice |
|
605 |
Functions |
|
66797 | 606 |
Function_Growth |
65549 | 607 |
Gauge_Integration |
608 |
Groebner_Examples |
|
609 |
Guess |
|
610 |
HarmonicSeries |
|
611 |
Hebrew |
|
612 |
Hex_Bin_Examples |
|
613 |
IArray_Examples |
|
614 |
Iff_Oracle |
|
615 |
Induction_Schema |
|
48481 | 616 |
Intuitionistic |
70525 | 617 |
Join_Theory |
65549 | 618 |
Lagrange |
619 |
List_to_Set_Comprehension_Examples |
|
620 |
LocaleTest2 |
|
67215 | 621 |
"ML" |
48481 | 622 |
MergeSort |
65549 | 623 |
MonoidGroup |
624 |
Multiquote |
|
625 |
NatSum |
|
626 |
Normalization_by_Evaluation |
|
627 |
PER |
|
628 |
Parallel_Example |
|
629 |
Peano_Axioms |
|
630 |
Perm_Fragments |
|
631 |
PresburgerEx |
|
48481 | 632 |
Primrec |
65549 | 633 |
Pythagoras |
634 |
Quicksort |
|
67612 | 635 |
Radix_Sort |
65549 | 636 |
Records |
637 |
Reflection_Examples |
|
638 |
Refute_Examples |
|
68035
6d7cc6723978
proof of concept for residue rings over int using type numerals
haftmann
parents:
68028
diff
changeset
|
639 |
Residue_Ring |
65549 | 640 |
Rewrite_Examples |
641 |
SOS |
|
642 |
SOS_Cert |
|
643 |
Seq |
|
644 |
Serbian |
|
645 |
Set_Comprehension_Pointfree_Examples |
|
48481 | 646 |
Set_Theory |
65549 | 647 |
Simproc_Tests |
648 |
Simps_Case_Conv_Examples |
|
70018
571909ef3103
experimental commands for proof sketching and exploration
haftmann
parents:
69926
diff
changeset
|
649 |
Sketch_and_Explore |
69252 | 650 |
Sorting_Algorithms_Examples |
48481 | 651 |
Sqrt |
652 |
Sqrt_Script |
|
65549 | 653 |
Sudoku |
654 |
Sum_of_Powers |
|
655 |
Tarski |
|
656 |
Termination |
|
657 |
ThreeDivides |
|
61368 | 658 |
Transfer_Debug |
48481 | 659 |
Transfer_Int_Nat |
56922 | 660 |
Transitive_Closure_Table_Ex |
65549 | 661 |
Tree23 |
69716 | 662 |
Triangular_Numbers |
65549 | 663 |
Unification |
664 |
While_Combinator_Example |
|
71042
400e9512f1d3
proof-of-concept theory for bit operations without a constructivistic representation and a minimal common logical foundation
haftmann
parents:
70958
diff
changeset
|
665 |
Word |
64978
5b9ba120d222
added veriT preprocessing proof reconstruction example
blanchet
parents:
64959
diff
changeset
|
666 |
veriT_Preprocessing |
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
|
667 |
theories [skip_proofs = false] |
67159 | 668 |
SAT_Examples |
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
|
669 |
Meson_Test |
48481 | 670 |
|
65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset
|
671 |
session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" + |
69319 | 672 |
description " |
61935 | 673 |
Miscellaneous Isabelle/Isar examples. |
69319 | 674 |
" |
61939 | 675 |
options [quick_and_dirty] |
48481 | 676 |
theories |
61939 | 677 |
Knaster_Tarski |
678 |
Peirce |
|
679 |
Drinker |
|
48481 | 680 |
Cantor |
61939 | 681 |
Structured_Statements |
682 |
Basic_Logic |
|
48481 | 683 |
Expr_Compiler |
684 |
Fibonacci |
|
685 |
Group |
|
686 |
Group_Context |
|
687 |
Group_Notepad |
|
688 |
Hoare_Ex |
|
689 |
Mutilated_Checkerboard |
|
690 |
Puzzle |
|
691 |
Summation |
|
61935 | 692 |
First_Order_Logic |
693 |
Higher_Order_Logic |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
694 |
document_files |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
695 |
"root.bib" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
696 |
"root.tex" |
48481 | 697 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
698 |
session "HOL-Eisbach" in Eisbach = HOL + |
69272 | 699 |
description \<open> |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
700 |
The Eisbach proof method language and "match" method. |
69319 | 701 |
\<close> |
66444 | 702 |
sessions |
703 |
FOL |
|
70958
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
70956
diff
changeset
|
704 |
"HOL-Analysis" |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
705 |
theories |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
706 |
Eisbach |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
707 |
Tests |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
708 |
Examples |
62168
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62155
diff
changeset
|
709 |
Examples_FOL |
70958
e8fc52f3f175
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
immler
parents:
70956
diff
changeset
|
710 |
Example_Metric |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
711 |
|
65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset
|
712 |
session "HOL-SET_Protocol" (timing) in SET_Protocol = "HOL-Library" + |
69319 | 713 |
description " |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
714 |
Verification of the SET Protocol. |
69319 | 715 |
" |
65543 | 716 |
theories |
717 |
SET_Protocol |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
718 |
document_files "root.tex" |
48481 | 719 |
|
65569
3cb6f3281ef1
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65563
diff
changeset
|
720 |
session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" + |
69319 | 721 |
description " |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
722 |
Two-dimensional matrices and linear programming. |
69319 | 723 |
" |
70675 | 724 |
directories "Compute_Oracle" |
48481 | 725 |
theories Cplex |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
726 |
document_files "root.tex" |
48481 | 727 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
728 |
session "HOL-TLA" in TLA = HOL + |
69319 | 729 |
description " |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
730 |
Lamport's Temporal Logic of Actions. |
69319 | 731 |
" |
48481 | 732 |
theories TLA |
733 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
734 |
session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" + |
48481 | 735 |
theories Inc |
736 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
737 |
session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" + |
48481 | 738 |
theories DBuffer |
739 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
740 |
session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" + |
48481 | 741 |
theories MemoryImplementation |
742 |
||
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
743 |
session "HOL-TPTP" in TPTP = "HOL-Library" + |
69319 | 744 |
description " |
48481 | 745 |
Author: Jasmin Blanchette, TU Muenchen |
746 |
Author: Nik Sultana, University of Cambridge |
|
747 |
Copyright 2011 |
|
748 |
||
749 |
TPTP-related extensions. |
|
69319 | 750 |
" |
48481 | 751 |
theories |
752 |
ATP_Theory_Export |
|
753 |
MaSh_Eval |
|
754 |
TPTP_Interpret |
|
755 |
THF_Arith |
|
55596
928b9f677165
reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
55450
diff
changeset
|
756 |
TPTP_Proof_Reconstruction |
52488
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
52424
diff
changeset
|
757 |
theories |
48481 | 758 |
ATP_Problem_Import |
759 |
||
65382 | 760 |
session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" + |
70781
a37e2ea96c6d
just one dump_checkpoint Main -- potentially more robust;
wenzelm
parents:
70678
diff
changeset
|
761 |
theories |
66992
69673025292e
less global theories -- avoid confusion about special cases;
wenzelm
parents:
66986
diff
changeset
|
762 |
Probability |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
763 |
document_files "root.tex" |
48481 | 764 |
|
63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset
|
765 |
session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" + |
61946
844881193616
put example into separate session, to restrict precious session image to library theories
haftmann
parents:
61939
diff
changeset
|
766 |
theories |
65538 | 767 |
Dining_Cryptographers |
768 |
Koepf_Duermuth_Countermeasure |
|
769 |
Measure_Not_CCC |
|
61946
844881193616
put example into separate session, to restrict precious session image to library theories
haftmann
parents:
61939
diff
changeset
|
770 |
|
66752 | 771 |
session "HOL-Nominal" in Nominal = "HOL-Library" + |
70781
a37e2ea96c6d
just one dump_checkpoint Main -- potentially more robust;
wenzelm
parents:
70678
diff
changeset
|
772 |
theories |
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
773 |
Nominal |
48481 | 774 |
|
63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset
|
775 |
session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" + |
58329
a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents:
58313
diff
changeset
|
776 |
theories |
59162
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
777 |
Class3 |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
778 |
CK_Machine |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
779 |
Compile |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
780 |
Contexts |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
781 |
Crary |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
782 |
CR_Takahashi |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
783 |
CR |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
784 |
Fsub |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
785 |
Height |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
786 |
Lambda_mu |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
787 |
Lam_Funs |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
788 |
LocalWeakening |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
789 |
Pattern |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
790 |
SN |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
791 |
SOS |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
792 |
Standardization |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
793 |
Support |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
794 |
Type_Preservation |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
795 |
Weakening |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
796 |
W |
58329
a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents:
58313
diff
changeset
|
797 |
theories [quick_and_dirty] |
a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents:
58313
diff
changeset
|
798 |
VC_Condition |
48481 | 799 |
|
70078 | 800 |
session "HOL-Cardinals" (timing) in Cardinals = HOL + |
69319 | 801 |
description " |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
802 |
Ordinals and Cardinals, Full Theories. |
69319 | 803 |
" |
59747 | 804 |
theories |
805 |
Cardinals |
|
806 |
Bounded_Set |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
807 |
document_files |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
808 |
"intro.tex" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
809 |
"root.tex" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
810 |
"root.bib" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
811 |
|
65574
10f4a17e5928
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65573
diff
changeset
|
812 |
session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" + |
69319 | 813 |
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
|
814 |
(Co)datatype Examples. |
69319 | 815 |
" |
70675 | 816 |
directories "Derivation_Trees" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
817 |
theories |
56454 | 818 |
Compat |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
819 |
Lambda_Term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
820 |
Process |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
821 |
TreeFsetI |
49872 | 822 |
"Derivation_Trees/Gram_Lang" |
65574
10f4a17e5928
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65573
diff
changeset
|
823 |
"Derivation_Trees/Parallel_Composition" |
50517 | 824 |
Koenig |
60921 | 825 |
Lift_BNF |
61745 | 826 |
Milner_Tofte |
54961 | 827 |
Stream_Processor |
71393
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
71352
diff
changeset
|
828 |
Cyclic_List |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
71352
diff
changeset
|
829 |
Free_Idempotent_Monoid |
fce780f9c9c6
new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents:
71352
diff
changeset
|
830 |
LDL |
71263
35a92ce0b94e
an extensive example for lift_bnf across quotients
traytel
parents:
71189
diff
changeset
|
831 |
TLList |
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset
|
832 |
Misc_Codatatype |
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset
|
833 |
Misc_Datatype |
54193 | 834 |
Misc_Primcorec |
53306 | 835 |
Misc_Primrec |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
836 |
|
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
837 |
session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" + |
69319 | 838 |
description " |
62694 | 839 |
Corecursion Examples. |
69319 | 840 |
" |
70675 | 841 |
directories "Tests" |
62694 | 842 |
theories |
843 |
LFilter |
|
62734 | 844 |
Paper_Examples |
62694 | 845 |
Stream_Processor |
62696 | 846 |
"Tests/Simple_Nesting" |
64379
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
64323
diff
changeset
|
847 |
"Tests/Iterate_GPV" |
62696 | 848 |
theories [quick_and_dirty] |
849 |
"Tests/GPV_Bare_Bones" |
|
850 |
"Tests/Merge_D" |
|
851 |
"Tests/Merge_Poly" |
|
852 |
"Tests/Misc_Mono" |
|
853 |
"Tests/Misc_Poly" |
|
854 |
"Tests/Small_Concrete" |
|
62725 | 855 |
"Tests/Stream_Friends" |
62696 | 856 |
"Tests/TLList_Friends" |
63190 | 857 |
"Tests/Type_Class" |
62694 | 858 |
|
63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset
|
859 |
session "HOL-Word" (main timing) in Word = HOL + |
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
860 |
sessions |
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
861 |
"HOL-Library" |
65382 | 862 |
theories |
65462
db1827610513
less global theories -- conflict with AFP entries;
wenzelm
parents:
65456
diff
changeset
|
863 |
Word |
70174 | 864 |
More_Word |
70173 | 865 |
Word_Examples |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
866 |
document_files "root.bib" "root.tex" |
48481 | 867 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
868 |
session "HOL-Statespace" 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
|
869 |
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
|
870 |
StateSpaceEx |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
871 |
document_files "root.tex" |
48481 | 872 |
|
65550
e957b1f00449
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65549
diff
changeset
|
873 |
session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" + |
69319 | 874 |
description " |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
875 |
Nonstandard analysis. |
69319 | 876 |
" |
62479 | 877 |
theories |
878 |
Nonstandard_Analysis |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
879 |
document_files "root.tex" |
48481 | 880 |
|
63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset
|
881 |
session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" + |
65543 | 882 |
theories |
883 |
NSPrimes |
|
48481 | 884 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
885 |
session "HOL-Mirabelle" in Mirabelle = HOL + |
48481 | 886 |
theories Mirabelle_Test |
48589
fb446a780d50
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
wenzelm
parents:
48588
diff
changeset
|
887 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
888 |
session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" + |
66946
3d8fd98c7c86
ROOT cleanup: empty 'document_files' means there is no document;
wenzelm
parents:
66932
diff
changeset
|
889 |
options [timeout = 60] |
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
|
890 |
theories Ex |
48481 | 891 |
|
63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset
|
892 |
session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" + |
66946
3d8fd98c7c86
ROOT cleanup: empty 'document_files' means there is no document;
wenzelm
parents:
66932
diff
changeset
|
893 |
options [quick_and_dirty] |
48481 | 894 |
theories |
52722 | 895 |
Boogie |
48481 | 896 |
SMT_Examples |
897 |
SMT_Word_Examples |
|
50666
6f48853f08d5
actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
blanchet
parents:
50665
diff
changeset
|
898 |
SMT_Tests |
48481 | 899 |
|
69093 | 900 |
session "HOL-SPARK" in "SPARK" = "HOL-Word" + |
65382 | 901 |
theories |
66992
69673025292e
less global theories -- avoid confusion about special cases;
wenzelm
parents:
66986
diff
changeset
|
902 |
SPARK |
48481 | 903 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
904 |
session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" + |
70675 | 905 |
directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt" |
48481 | 906 |
theories |
907 |
"Gcd/Greatest_Common_Divisor" |
|
908 |
"Liseq/Longest_Increasing_Subsequence" |
|
909 |
"RIPEMD-160/F" |
|
910 |
"RIPEMD-160/Hash" |
|
911 |
"RIPEMD-160/K_L" |
|
912 |
"RIPEMD-160/K_R" |
|
913 |
"RIPEMD-160/R_L" |
|
914 |
"RIPEMD-160/Round" |
|
915 |
"RIPEMD-160/R_R" |
|
916 |
"RIPEMD-160/S_L" |
|
917 |
"RIPEMD-160/S_R" |
|
918 |
"Sqrt/Sqrt" |
|
70026 | 919 |
export_files (in ".") "*:**.prv" |
48481 | 920 |
|
65576 | 921 |
session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" + |
69099
d44cb8a3e5e0
HOL-SPARK .prv files are no longer written to the file-system;
wenzelm
parents:
69093
diff
changeset
|
922 |
options [show_question_marks = false] |
66031 | 923 |
sessions |
924 |
"HOL-SPARK-Examples" |
|
48481 | 925 |
theories |
926 |
Example_Verification |
|
927 |
VC_Principles |
|
928 |
Reference |
|
929 |
Complex_Types |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
930 |
document_files |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
931 |
"complex_types.ads" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
932 |
"complex_types_app.adb" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
933 |
"complex_types_app.ads" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
934 |
"Gcd.adb" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
935 |
"Gcd.ads" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
936 |
"intro.tex" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
937 |
"loop_invariant.adb" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
938 |
"loop_invariant.ads" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
939 |
"root.bib" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
940 |
"root.tex" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
941 |
"Simple_Gcd.adb" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
942 |
"Simple_Gcd.ads" |
48481 | 943 |
|
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
944 |
session "HOL-Mutabelle" in Mutabelle = "HOL-Library" + |
48481 | 945 |
theories MutabelleExtra |
946 |
||
65569
3cb6f3281ef1
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65563
diff
changeset
|
947 |
session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" + |
48588 | 948 |
theories |
48690 | 949 |
Quickcheck_Examples |
950 |
Quickcheck_Lattice_Examples |
|
951 |
Completeness |
|
952 |
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
|
953 |
Quickcheck_Nesting_Example |
57584
155b7e3b729e
proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
wenzelm
parents:
57544
diff
changeset
|
954 |
theories [condition = ISABELLE_GHC] |
57544
8840fa17e17c
reactivate session Quickcheck_Examples
Andreas Lochbihler
parents:
57543
diff
changeset
|
955 |
Hotel_Example |
48598 | 956 |
Quickcheck_Narrowing_Examples |
48588 | 957 |
|
65569
3cb6f3281ef1
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65563
diff
changeset
|
958 |
session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" + |
69319 | 959 |
description " |
48481 | 960 |
Author: Cezary Kaliszyk and Christian Urban |
69319 | 961 |
" |
48481 | 962 |
theories |
963 |
DList |
|
63920
003622e08379
resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
kuncar
parents:
63888
diff
changeset
|
964 |
Quotient_FSet |
48481 | 965 |
Quotient_Int |
966 |
Quotient_Message |
|
967 |
Lift_FSet |
|
968 |
Lift_Set |
|
969 |
Lift_Fun |
|
970 |
Quotient_Rat |
|
971 |
Lift_DList |
|
53682
1b55aeda0e46
include Int_Pow into Quotient_Examples; add end of the theory
kuncar
parents:
53430
diff
changeset
|
972 |
Int_Pow |
60237 | 973 |
Lifting_Code_Dt_Test |
48481 | 974 |
|
65569
3cb6f3281ef1
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65563
diff
changeset
|
975 |
session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" + |
62354 | 976 |
theories |
48481 | 977 |
Examples |
978 |
Predicate_Compile_Tests |
|
61140
78ece168f5b5
reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents:
60921
diff
changeset
|
979 |
Predicate_Compile_Quickcheck_Examples |
48481 | 980 |
Specialisation_Examples |
48690 | 981 |
IMP_1 |
982 |
IMP_2 |
|
55450
9eddc17749f7
reactivate some examples that still appear to work;
wenzelm
parents:
55447
diff
changeset
|
983 |
(* FIXME since 21-Jul-2011 |
61140
78ece168f5b5
reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents:
60921
diff
changeset
|
984 |
Hotel_Example_Small_Generator *) |
48690 | 985 |
IMP_3 |
61140
78ece168f5b5
reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents:
60921
diff
changeset
|
986 |
IMP_4 |
62242
a4e6ea45f416
guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents:
62168
diff
changeset
|
987 |
theories [condition = ISABELLE_SWIPL] |
48690 | 988 |
Code_Prolog_Examples |
989 |
Context_Free_Grammar_Example |
|
990 |
Hotel_Example_Prolog |
|
991 |
Lambda_Example |
|
992 |
List_Examples |
|
62242
a4e6ea45f416
guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents:
62168
diff
changeset
|
993 |
theories [condition = ISABELLE_SWIPL, quick_and_dirty] |
48690 | 994 |
Reg_Exp_Example |
48481 | 995 |
|
64551 | 996 |
session "HOL-Types_To_Sets" in Types_To_Sets = HOL + |
69319 | 997 |
description " |
64551 | 998 |
Experimental extension of Higher-Order Logic to allow translation of types to sets. |
69319 | 999 |
" |
70675 | 1000 |
directories "Examples" |
64551 | 1001 |
theories |
1002 |
Types_To_Sets |
|
1003 |
"Examples/Prerequisites" |
|
1004 |
"Examples/Finite" |
|
1005 |
"Examples/T2_Spaces" |
|
69689 | 1006 |
"Examples/Unoverload_Def" |
68522
d9cbc1e8644d
example for Types_To_Sets: transfer from type-based linear algebra to subspaces
immler
parents:
68516
diff
changeset
|
1007 |
"Examples/Linear_Algebra_On" |
64551 | 1008 |
|
66982
67595389aa8a
build faster without heap images for minor imports;
wenzelm
parents:
66956
diff
changeset
|
1009 |
session HOLCF (main timing) in HOLCF = HOL + |
69319 | 1010 |
description " |
48338 | 1011 |
Author: Franz Regensburger |
1012 |
Author: Brian Huffman |
|
1013 |
||
1014 |
HOLCF -- a semantic extension of HOL by the LCF logic. |
|
69319 | 1015 |
" |
66982
67595389aa8a
build faster without heap images for minor imports;
wenzelm
parents:
66956
diff
changeset
|
1016 |
sessions |
67595389aa8a
build faster without heap images for minor imports;
wenzelm
parents:
66956
diff
changeset
|
1017 |
"HOL-Library" |
48481 | 1018 |
theories |
65382 | 1019 |
HOLCF (global) |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
1020 |
document_files "root.tex" |
48481 | 1021 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1022 |
session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF + |
48481 | 1023 |
theories |
1024 |
Domain_ex |
|
1025 |
Fixrec_ex |
|
1026 |
New_Domain |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
1027 |
document_files "root.tex" |
48481 | 1028 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1029 |
session "HOLCF-Library" in "HOLCF/Library" = HOLCF + |
65570 | 1030 |
theories |
1031 |
HOLCF_Library |
|
1032 |
HOL_Cpo |
|
48481 | 1033 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1034 |
session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF + |
69319 | 1035 |
description " |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1036 |
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
|
1037 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1038 |
This is the HOLCF-based denotational semantics of a simple WHILE-language. |
69319 | 1039 |
" |
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
1040 |
sessions |
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
1041 |
"HOL-IMP" |
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
1042 |
theories |
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
1043 |
HoareEx |
66950 | 1044 |
document_files |
1045 |
"isaverbatimwrite.sty" |
|
1046 |
"root.tex" |
|
1047 |
"root.bib" |
|
48338 | 1048 |
|
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
1049 |
session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" + |
69319 | 1050 |
description " |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
1051 |
Miscellaneous examples for HOLCF. |
69319 | 1052 |
" |
48481 | 1053 |
theories |
1054 |
Dnat |
|
1055 |
Dagstuhl |
|
1056 |
Focus_ex |
|
1057 |
Fix2 |
|
1058 |
Hoare |
|
1059 |
Concurrency_Monad |
|
1060 |
Loop |
|
1061 |
Powerdomain_ex |
|
1062 |
Domain_Proofs |
|
1063 |
Letrec |
|
1064 |
Pattern_Match |
|
1065 |
||
65573
0f3fdf689bf9
clarified parent session images, to avoid duplicate loading of theories;
wenzelm
parents:
65570
diff
changeset
|
1066 |
session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" + |
69272 | 1067 |
description \<open> |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1068 |
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
|
1069 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1070 |
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
|
1071 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1072 |
"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
|
1073 |
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
|
1074 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1075 |
"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
|
1076 |
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
|
1077 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1078 |
"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
|
1079 |
Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321 |
69319 | 1080 |
\<close> |
48481 | 1081 |
theories |
1082 |
Fstreams |
|
1083 |
FOCUS |
|
1084 |
Buffer_adm |
|
1085 |
||
63888
5a9a1985e9fb
sessions that are relevant for routine timing measurements;
wenzelm
parents:
63885
diff
changeset
|
1086 |
session IOA (timing) in "HOLCF/IOA" = HOLCF + |
69319 | 1087 |
description " |
48481 | 1088 |
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
|
1089 |
Copyright 1997 TU München |
48481 | 1090 |
|
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1091 |
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
|
1092 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1093 |
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
|
1094 |
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
|
1095 |
finite and infinite sequences. |
69319 | 1096 |
" |
65538 | 1097 |
theories Abstraction |
48481 | 1098 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1099 |
session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA + |
69319 | 1100 |
description " |
48481 | 1101 |
Author: Olaf Mueller |
1102 |
||
1103 |
The Alternating Bit Protocol performed in I/O-Automata. |
|
69319 | 1104 |
" |
59503 | 1105 |
theories |
1106 |
Correctness |
|
1107 |
Spec |
|
48481 | 1108 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1109 |
session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA + |
69319 | 1110 |
description " |
48481 | 1111 |
Author: Tobias Nipkow & Konrad Slind |
1112 |
||
1113 |
A network transmission protocol, performed in the |
|
1114 |
I/O automata formalization by Olaf Mueller. |
|
69319 | 1115 |
" |
48481 | 1116 |
theories Correctness |
1117 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1118 |
session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA + |
69319 | 1119 |
description " |
48481 | 1120 |
Author: Olaf Mueller |
1121 |
||
1122 |
Memory storage case study. |
|
69319 | 1123 |
" |
48481 | 1124 |
theories Correctness |
1125 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1126 |
session "IOA-ex" in "HOLCF/IOA/ex" = IOA + |
69319 | 1127 |
description " |
48481 | 1128 |
Author: Olaf Mueller |
69319 | 1129 |
" |
48481 | 1130 |
theories |
1131 |
TrivEx |
|
1132 |
TrivEx2 |