author | eberlm <eberlm@in.tum.de> |
Fri, 22 Jul 2016 17:35:54 +0200 | |
changeset 63537 | 831816778409 |
parent 63498 | a3fe3250d05d |
child 63538 | d7b5e2a222c2 |
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 + |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
4 |
description {* |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
5 |
Classical Higher-order Logic. |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
6 |
*} |
56801
8dd9df88f647
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents:
56781
diff
changeset
|
7 |
global_theories |
8dd9df88f647
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents:
56781
diff
changeset
|
8 |
Main |
8dd9df88f647
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents:
56781
diff
changeset
|
9 |
Complex_Main |
48901
5e0455e29339
more basic file dependencies -- no load command here;
wenzelm
parents:
48765
diff
changeset
|
10 |
files |
5e0455e29339
more basic file dependencies -- no load command here;
wenzelm
parents:
48765
diff
changeset
|
11 |
"Tools/Quickcheck/Narrowing_Engine.hs" |
5e0455e29339
more basic file dependencies -- no load command here;
wenzelm
parents:
48765
diff
changeset
|
12 |
"Tools/Quickcheck/PNF_Narrowing_Engine.hs" |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
13 |
document_files |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
14 |
"root.bib" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
15 |
"root.tex" |
48338 | 16 |
|
63000
d0dfdd413a7f
remove "slow" session tags
Lars Hupel <lars.hupel@mytum.de>
parents:
62999
diff
changeset
|
17 |
session "HOL-Proofs" = Pure + |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
18 |
description {* |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
19 |
HOL-Main with explicit proof terms. |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
20 |
*} |
62354 | 21 |
options [document = false, quick_and_dirty = false] |
52488
cd65ee49a8ba
discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image;
wenzelm
parents:
52424
diff
changeset
|
22 |
theories Proofs (*sequential change of global flag!*) |
58372
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents:
58371
diff
changeset
|
23 |
theories "~~/src/HOL/Library/Old_Datatype" |
48901
5e0455e29339
more basic file dependencies -- no load command here;
wenzelm
parents:
48765
diff
changeset
|
24 |
files |
5e0455e29339
more basic file dependencies -- no load command here;
wenzelm
parents:
48765
diff
changeset
|
25 |
"Tools/Quickcheck/Narrowing_Engine.hs" |
5e0455e29339
more basic file dependencies -- no load command here;
wenzelm
parents:
48765
diff
changeset
|
26 |
"Tools/Quickcheck/PNF_Narrowing_Engine.hs" |
48338 | 27 |
|
50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset
|
28 |
session "HOL-Library" (main) in Library = HOL + |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
29 |
description {* |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
30 |
Classical Higher-order Logic -- batteries included. |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
31 |
*} |
48481 | 32 |
theories |
33 |
Library |
|
59973 | 34 |
Rewrite |
63091 | 35 |
Nonpos_Ints |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
36 |
(*conflicting type class instantiations*) |
48481 | 37 |
List_lexord |
38 |
Sublist_Order |
|
51115
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51093
diff
changeset
|
39 |
Product_Lexorder |
7dbd6832a689
consolidation of library theories on product orders
haftmann
parents:
51093
diff
changeset
|
40 |
Product_Order |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
41 |
Finite_Lattice |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
42 |
(*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
|
43 |
AList_Mapping |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
44 |
Code_Binary_Nat |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
45 |
Code_Char |
55447 | 46 |
Code_Prolog |
48481 | 47 |
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
|
48 |
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
|
49 |
DAList |
54429
be1bc181bcde
explicit inclusion of data refinement theory into HOL-Library session
haftmann
parents:
54193
diff
changeset
|
50 |
DAList_Multiset |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
51 |
RBT_Mapping |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
52 |
RBT_Set |
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
53 |
(*legacy tools*) |
49985
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49932
diff
changeset
|
54 |
Refute |
58372
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents:
58371
diff
changeset
|
55 |
Old_Datatype |
51161
6ed12ae3b3e1
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
51160
diff
changeset
|
56 |
Old_Recdef |
58110
019c0211ed1f
took out legacy material from 'HOL/Library/Library.thy'
blanchet
parents:
58039
diff
changeset
|
57 |
Old_SMT |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
58 |
document_files "root.bib" "root.tex" |
48481 | 59 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
60 |
session "HOL-Hahn_Banach" in Hahn_Banach = HOL + |
48481 | 61 |
description {* |
62 |
Author: Gertrud Bauer, TU Munich |
|
63 |
||
64 |
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
|
65 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
66 |
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
|
67 |
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
|
68 |
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
|
69 |
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
|
70 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
71 |
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
|
72 |
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
|
73 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
74 |
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
|
75 |
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
|
76 |
continous linearform on the whole vectorspace. |
48481 | 77 |
*} |
78 |
theories Hahn_Banach |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
79 |
document_files "root.bib" "root.tex" |
48481 | 80 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
81 |
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
|
82 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
83 |
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
|
84 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
85 |
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
|
86 |
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
|
87 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
88 |
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
|
89 |
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
|
90 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
91 |
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
|
92 |
(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
|
93 |
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
|
94 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
95 |
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
|
96 |
mutually recursive relations. |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
97 |
*} |
58372
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents:
58371
diff
changeset
|
98 |
theories [document = false] |
bfd497f2f4c2
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
blanchet
parents:
58371
diff
changeset
|
99 |
"~~/src/HOL/Library/Old_Datatype" |
48481 | 100 |
theories [quick_and_dirty] |
101 |
Common_Patterns |
|
102 |
theories |
|
61935 | 103 |
Nested_Datatype |
48481 | 104 |
QuoDataType |
105 |
QuoNestedDataType |
|
106 |
Term |
|
107 |
SList |
|
108 |
ABexp |
|
109 |
Tree |
|
110 |
Ordinals |
|
111 |
Sigma_Algebra |
|
112 |
Comb |
|
113 |
PropLog |
|
114 |
Com |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
115 |
document_files "root.tex" |
48481 | 116 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
117 |
session "HOL-IMP" in IMP = HOL + |
59446 | 118 |
options [document_variants = document] |
48481 | 119 |
theories [document = false] |
120 |
"~~/src/HOL/Library/While_Combinator" |
|
121 |
"~~/src/HOL/Library/Char_ord" |
|
122 |
"~~/src/HOL/Library/List_lexord" |
|
51625 | 123 |
"~~/src/HOL/Library/Quotient_List" |
124 |
"~~/src/HOL/Library/Extended" |
|
48481 | 125 |
theories |
126 |
BExp |
|
127 |
ASM |
|
50050 | 128 |
Finite_Reachable |
52394 | 129 |
Denotational |
52400 | 130 |
Compiler2 |
48481 | 131 |
Poly_Types |
132 |
Sec_Typing |
|
133 |
Sec_TypingT |
|
52726 | 134 |
Def_Init_Big |
135 |
Def_Init_Small |
|
136 |
Fold |
|
48481 | 137 |
Live |
138 |
Live_True |
|
139 |
Hoare_Examples |
|
52269 | 140 |
VCG |
52282 | 141 |
Hoare_Total |
63070 | 142 |
Hoare_Total_EX |
48481 | 143 |
Collecting1 |
48765
fb1ed5230abc
special code with lists no longer necessary, use sets
nipkow
parents:
48738
diff
changeset
|
144 |
Collecting_Examples |
48481 | 145 |
Abs_Int_Tests |
146 |
Abs_Int1_parity |
|
147 |
Abs_Int1_const |
|
148 |
Abs_Int3 |
|
149 |
"Abs_Int_ITP/Abs_Int1_parity_ITP" |
|
150 |
"Abs_Int_ITP/Abs_Int1_const_ITP" |
|
151 |
"Abs_Int_ITP/Abs_Int3_ITP" |
|
152 |
Procs_Dyn_Vars_Dyn |
|
153 |
Procs_Stat_Vars_Dyn |
|
154 |
Procs_Stat_Vars_Stat |
|
155 |
C_like |
|
156 |
OO |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
157 |
document_files "root.bib" "root.tex" |
48481 | 158 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
159 |
session "HOL-IMPP" in IMPP = HOL + |
48481 | 160 |
description {* |
161 |
Author: David von Oheimb |
|
162 |
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
|
163 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
164 |
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
|
165 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
166 |
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
|
167 |
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
|
168 |
Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). |
48481 | 169 |
*} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
170 |
options [document = false] |
48481 | 171 |
theories EvenOdd |
172 |
||
61203 | 173 |
session "HOL-Data_Structures" in Data_Structures = HOL + |
174 |
options [document_variants = document] |
|
175 |
theories [document = false] |
|
176 |
"Less_False" |
|
62706 | 177 |
"~~/src/HOL/Library/Multiset" |
61203 | 178 |
theories |
179 |
Tree_Map |
|
61232 | 180 |
AVL_Map |
61224 | 181 |
RBT_Map |
61469
cd82b1023932
added 2-3 trees (simpler and more complete than the version in ex/Tree23)
nipkow
parents:
61368
diff
changeset
|
182 |
Tree23_Map |
61514 | 183 |
Tree234_Map |
61789 | 184 |
Brother12_Map |
62130 | 185 |
AA_Map |
61525 | 186 |
Splay_Map |
62706 | 187 |
Leftist_Heap |
61224 | 188 |
document_files "root.tex" "root.bib" |
61203 | 189 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
190 |
session "HOL-Import" in Import = HOL + |
48481 | 191 |
theories HOL_Light_Maps |
192 |
theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import |
|
193 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
194 |
session "HOL-Number_Theory" in Number_Theory = HOL + |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset
|
195 |
description {* |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset
|
196 |
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
|
197 |
Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity. |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset
|
198 |
*} |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset
|
199 |
theories [document = false] |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset
|
200 |
"~~/src/HOL/Library/FuncSet" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset
|
201 |
"~~/src/HOL/Library/Multiset" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset
|
202 |
"~~/src/HOL/Algebra/Ring" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset
|
203 |
"~~/src/HOL/Algebra/FiniteProduct" |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset
|
204 |
theories |
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset
|
205 |
Pocklington |
55730
97ff9276e12d
Gauss.thy ported from Old_Number_Theory (unfinished)
paulson <lp15@cam.ac.uk>
parents:
55663
diff
changeset
|
206 |
Gauss |
55321
eadea363deb6
Restoration of Pocklington.thy. Tidying.
paulson <lp15@cam.ac.uk>
parents:
55240
diff
changeset
|
207 |
Number_Theory |
58023
62826b36ac5e
generic euclidean algorithm (due to Manuel Eberl)
haftmann
parents:
57998
diff
changeset
|
208 |
Euclidean_Algorithm |
60804 | 209 |
Factorial_Ring |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
210 |
document_files |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
211 |
"root.tex" |
48481 | 212 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
213 |
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
|
214 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
215 |
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
|
216 |
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
|
217 |
*} |
48481 | 218 |
theories [document = false] |
219 |
"~~/src/HOL/Library/Infinite_Set" |
|
220 |
"~~/src/HOL/Library/Permutation" |
|
221 |
theories |
|
222 |
Fib |
|
223 |
Factorization |
|
224 |
Chinese |
|
225 |
WilsonRuss |
|
226 |
WilsonBij |
|
227 |
Quadratic_Reciprocity |
|
228 |
Primes |
|
229 |
Pocklington |
|
58623 | 230 |
document_files |
231 |
"root.bib" |
|
232 |
"root.tex" |
|
48481 | 233 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
234 |
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
|
235 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
236 |
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
|
237 |
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
|
238 |
*} |
48481 | 239 |
theories Hoare |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
240 |
document_files "root.bib" "root.tex" |
48481 | 241 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
242 |
session "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
|
243 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
244 |
Verification of 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
|
245 |
(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
|
246 |
*} |
48481 | 247 |
theories Hoare_Parallel |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
248 |
document_files "root.bib" "root.tex" |
48481 | 249 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
250 |
session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" + |
62354 | 251 |
options [document = false, browser_info = false] |
51422
821a70e29e0b
proper formatting, to facilitate line-based diff;
wenzelm
parents:
51421
diff
changeset
|
252 |
theories |
821a70e29e0b
proper formatting, to facilitate line-based diff;
wenzelm
parents:
51421
diff
changeset
|
253 |
Generate |
821a70e29e0b
proper formatting, to facilitate line-based diff;
wenzelm
parents:
51421
diff
changeset
|
254 |
Generate_Binary_Nat |
821a70e29e0b
proper formatting, to facilitate line-based diff;
wenzelm
parents:
51421
diff
changeset
|
255 |
Generate_Target_Nat |
821a70e29e0b
proper formatting, to facilitate line-based diff;
wenzelm
parents:
51421
diff
changeset
|
256 |
Generate_Efficient_Datastructures |
821a70e29e0b
proper formatting, to facilitate line-based diff;
wenzelm
parents:
51421
diff
changeset
|
257 |
Generate_Pretty_Char |
62354 | 258 |
theories [condition = "ISABELLE_GHC"] |
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset
|
259 |
Code_Test_GHC |
62354 | 260 |
theories [condition = "ISABELLE_MLTON"] |
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset
|
261 |
Code_Test_MLton |
62354 | 262 |
theories [condition = "ISABELLE_OCAMLC"] |
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset
|
263 |
Code_Test_OCaml |
62354 | 264 |
theories [condition = "ISABELLE_POLYML"] |
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset
|
265 |
Code_Test_PolyML |
62354 | 266 |
theories [condition = "ISABELLE_SCALA"] |
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset
|
267 |
Code_Test_Scala |
62354 | 268 |
theories [condition = "ISABELLE_SMLNJ"] |
58039
469a375212c1
add testing framework for generated code
Andreas Lochbihler
parents:
58023
diff
changeset
|
269 |
Code_Test_SMLNJ |
48481 | 270 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
271 |
session "HOL-Metis_Examples" in Metis_Examples = HOL + |
48481 | 272 |
description {* |
273 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
274 |
Author: Jasmin Blanchette, TU Muenchen |
|
275 |
||
276 |
Testing Metis and Sledgehammer. |
|
277 |
*} |
|
58423 | 278 |
options [document = false] |
48481 | 279 |
theories |
280 |
Abstraction |
|
281 |
Big_O |
|
282 |
Binary_Tree |
|
283 |
Clausification |
|
284 |
Message |
|
285 |
Proxies |
|
286 |
Tarski |
|
287 |
Trans_Closure |
|
288 |
Sets |
|
289 |
||
55072 | 290 |
session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL + |
48481 | 291 |
description {* |
292 |
Author: Jasmin Blanchette, TU Muenchen |
|
293 |
Copyright 2009 |
|
294 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
295 |
options [document = false] |
48481 | 296 |
theories [quick_and_dirty] Nitpick_Examples |
297 |
||
50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset
|
298 |
session "HOL-Algebra" (main) in Algebra = HOL + |
48481 | 299 |
description {* |
300 |
Author: Clemens Ballarin, started 24 September 1999 |
|
301 |
||
302 |
The Isabelle Algebraic Library. |
|
303 |
*} |
|
304 |
theories [document = false] |
|
305 |
(* Preliminaries from set and number theory *) |
|
306 |
"~~/src/HOL/Library/FuncSet" |
|
55159
608c157d743d
Replacing the theory Library/Binomial by Number_Theory/Binomial
paulson <lp15@cam.ac.uk>
parents:
55123
diff
changeset
|
307 |
"~~/src/HOL/Number_Theory/Primes" |
48481 | 308 |
"~~/src/HOL/Library/Permutation" |
309 |
theories |
|
310 |
(*** New development, based on explicit structures ***) |
|
311 |
(* Groups *) |
|
312 |
FiniteProduct (* Product operator for commutative groups *) |
|
313 |
Sylow (* Sylow's theorem *) |
|
314 |
Bij (* Automorphism Groups *) |
|
315 |
||
316 |
(* Rings *) |
|
317 |
Divisibility (* Rings *) |
|
318 |
IntRing (* Ideals and residue classes *) |
|
319 |
UnivPoly (* Polynomials *) |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
320 |
document_files "root.bib" "root.tex" |
48481 | 321 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
322 |
session "HOL-Auth" in Auth = HOL + |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
323 |
description {* |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
324 |
A new approach to verifying authentication protocols. |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
325 |
*} |
48481 | 326 |
theories |
327 |
Auth_Shared |
|
328 |
Auth_Public |
|
329 |
"Smartcard/Auth_Smartcard" |
|
330 |
"Guard/Auth_Guard_Shared" |
|
331 |
"Guard/Auth_Guard_Public" |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
332 |
document_files "root.tex" |
48481 | 333 |
|
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
|
334 |
session "HOL-UNITY" in UNITY = "HOL-Auth" + |
48481 | 335 |
description {* |
336 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
337 |
Copyright 1998 University of Cambridge |
|
338 |
||
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
339 |
Verifying security protocols using Chandy and Misra's UNITY formalism. |
48481 | 340 |
*} |
341 |
theories |
|
342 |
(*Basic meta-theory*) |
|
343 |
"UNITY_Main" |
|
344 |
||
345 |
(*Simple examples: no composition*) |
|
346 |
"Simple/Deadlock" |
|
347 |
"Simple/Common" |
|
348 |
"Simple/Network" |
|
349 |
"Simple/Token" |
|
350 |
"Simple/Channel" |
|
351 |
"Simple/Lift" |
|
352 |
"Simple/Mutex" |
|
353 |
"Simple/Reach" |
|
354 |
"Simple/Reachability" |
|
355 |
||
356 |
(*Verifying security protocols using UNITY*) |
|
357 |
"Simple/NSP_Bad" |
|
358 |
||
359 |
(*Example of composition*) |
|
360 |
"Comp/Handshake" |
|
361 |
||
362 |
(*Universal properties examples*) |
|
363 |
"Comp/Counter" |
|
364 |
"Comp/Counterc" |
|
365 |
"Comp/Priority" |
|
366 |
||
367 |
"Comp/TimerArray" |
|
368 |
"Comp/Progress" |
|
369 |
||
370 |
"Comp/Alloc" |
|
371 |
"Comp/AllocImpl" |
|
372 |
"Comp/Client" |
|
373 |
||
374 |
(*obsolete*) |
|
375 |
"ELT" |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
376 |
document_files "root.tex" |
48481 | 377 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
378 |
session "HOL-Unix" in Unix = HOL + |
48481 | 379 |
options [print_mode = "no_brackets,no_type_brackets"] |
380 |
theories Unix |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
381 |
document_files "root.bib" "root.tex" |
48481 | 382 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
383 |
session "HOL-ZF" in ZF = HOL + |
48481 | 384 |
theories MainZF Games |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
385 |
document_files "root.tex" |
48481 | 386 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
387 |
session "HOL-Imperative_HOL" in Imperative_HOL = HOL + |
59446 | 388 |
options [print_mode = "iff,no_brackets"] |
48481 | 389 |
theories [document = false] |
390 |
"~~/src/HOL/Library/Countable" |
|
391 |
"~~/src/HOL/Library/Monad_Syntax" |
|
392 |
"~~/src/HOL/Library/LaTeXsugar" |
|
393 |
theories Imperative_HOL_ex |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
394 |
document_files "root.bib" "root.tex" |
48481 | 395 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
396 |
session "HOL-Decision_Procs" in Decision_Procs = HOL + |
51544 | 397 |
description {* |
398 |
Various decision procedures, typically involving reflection. |
|
399 |
*} |
|
62354 | 400 |
options [document = false] |
48481 | 401 |
theories Decision_Procs |
402 |
||
63000
d0dfdd413a7f
remove "slow" session tags
Lars Hupel <lars.hupel@mytum.de>
parents:
62999
diff
changeset
|
403 |
session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + |
62354 | 404 |
options [document = false, parallel_proofs = 0] |
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
52400
diff
changeset
|
405 |
theories |
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
52400
diff
changeset
|
406 |
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
|
407 |
Proof_Terms |
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
52400
diff
changeset
|
408 |
XML_Data |
48481 | 409 |
|
63000
d0dfdd413a7f
remove "slow" session tags
Lars Hupel <lars.hupel@mytum.de>
parents:
62999
diff
changeset
|
410 |
session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" + |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
411 |
description {* |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
412 |
Examples for program extraction in Higher-Order Logic. |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
413 |
*} |
62354 | 414 |
options [parallel_proofs = 0, quick_and_dirty = false] |
48481 | 415 |
theories [document = false] |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51115
diff
changeset
|
416 |
"~~/src/HOL/Library/Code_Target_Numeral" |
48481 | 417 |
"~~/src/HOL/Library/Monad_Syntax" |
418 |
"~~/src/HOL/Number_Theory/Primes" |
|
419 |
"~~/src/HOL/Library/State_Monad" |
|
420 |
theories |
|
421 |
Greatest_Common_Divisor |
|
422 |
Warshall |
|
423 |
Higman_Extraction |
|
424 |
Pigeonhole |
|
425 |
Euclid |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
426 |
document_files "root.bib" "root.tex" |
48481 | 427 |
|
63000
d0dfdd413a7f
remove "slow" session tags
Lars Hupel <lars.hupel@mytum.de>
parents:
62999
diff
changeset
|
428 |
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
|
429 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
430 |
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
|
431 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
432 |
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
|
433 |
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
|
434 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
435 |
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
|
436 |
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
|
437 |
*} |
62354 | 438 |
options [print_mode = "no_brackets", |
62242
a4e6ea45f416
guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents:
62168
diff
changeset
|
439 |
parallel_proofs = 0, quick_and_dirty = false] |
48481 | 440 |
theories [document = false] |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51115
diff
changeset
|
441 |
"~~/src/HOL/Library/Code_Target_Int" |
48481 | 442 |
theories |
443 |
Eta |
|
444 |
StrongNorm |
|
445 |
Standardization |
|
446 |
WeakNorm |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
447 |
document_files "root.bib" "root.tex" |
48481 | 448 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
449 |
session "HOL-Prolog" in Prolog = HOL + |
48481 | 450 |
description {* |
451 |
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
|
452 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
453 |
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
|
454 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
455 |
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
|
456 |
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
|
457 |
a little functional language and its type system. |
48481 | 458 |
*} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
459 |
options [document = false] |
48481 | 460 |
theories Test Type |
461 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
462 |
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
|
463 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
464 |
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
|
465 |
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
|
466 |
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
|
467 |
*} |
59446 | 468 |
theories [document = false] |
469 |
"~~/src/HOL/Library/While_Combinator" |
|
470 |
theories |
|
471 |
MicroJava |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
472 |
document_files |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
473 |
"introduction.tex" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
474 |
"root.bib" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
475 |
"root.tex" |
48481 | 476 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
477 |
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
|
478 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
479 |
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
|
480 |
*} |
48481 | 481 |
theories Example |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
482 |
document_files "root.bib" "root.tex" |
48481 | 483 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
484 |
session "HOL-Bali" in Bali = HOL + |
48481 | 485 |
theories |
486 |
AxExample |
|
487 |
AxSound |
|
488 |
AxCompl |
|
489 |
Trans |
|
60751 | 490 |
TypeSafe |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
491 |
document_files "root.tex" |
48481 | 492 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
493 |
session "HOL-IOA" in IOA = HOL + |
48481 | 494 |
description {* |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
495 |
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
|
496 |
Copyright 1994--1996 TU Muenchen |
48481 | 497 |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55370
diff
changeset
|
498 |
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
|
499 |
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
|
500 |
proofs of two communication protocols which formerly have been here. |
48481 | 501 |
|
502 |
@inproceedings{Nipkow-Slind-IOA, |
|
503 |
author={Tobias Nipkow and Konrad Slind}, |
|
504 |
title={{I/O} Automata in {Isabelle/HOL}}, |
|
505 |
booktitle={Proc.\ TYPES Workshop 1994}, |
|
506 |
publisher=Springer, |
|
507 |
series=LNCS, |
|
508 |
note={To appear}} |
|
509 |
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz |
|
510 |
||
511 |
and |
|
512 |
||
513 |
@inproceedings{Mueller-Nipkow, |
|
514 |
author={Olaf M\"uller and Tobias Nipkow}, |
|
515 |
title={Combining Model Checking and Deduction for {I/O}-Automata}, |
|
516 |
booktitle={Proc.\ TACAS Workshop}, |
|
517 |
organization={Aarhus University, BRICS report}, |
|
518 |
year=1995} |
|
519 |
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz |
|
520 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
521 |
options [document = false] |
48481 | 522 |
theories Solve |
523 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
524 |
session "HOL-Lattice" in Lattice = HOL + |
48481 | 525 |
description {* |
526 |
Author: Markus Wenzel, TU Muenchen |
|
527 |
||
528 |
Basic theory of lattices and orders. |
|
529 |
*} |
|
530 |
theories CompleteLattice |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
531 |
document_files "root.tex" |
48481 | 532 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
533 |
session "HOL-ex" in ex = HOL + |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
534 |
description {* |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
535 |
Miscellaneous examples for Higher-Order Logic. |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
536 |
*} |
48481 | 537 |
theories [document = false] |
538 |
"~~/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
|
539 |
Code_Binary_Nat_examples |
48481 | 540 |
"~~/src/HOL/Library/FuncSet" |
541 |
Eval_Examples |
|
542 |
Normalization_by_Evaluation |
|
543 |
Hebrew |
|
544 |
Chinese |
|
545 |
Serbian |
|
49985
5b4b0e4e5205
moved Refute to "HOL/Library" to speed up building "Main" even more
blanchet
parents:
49932
diff
changeset
|
546 |
"~~/src/HOL/Library/Refute" |
56922 | 547 |
"~~/src/HOL/Library/Transitive_Closure_Table" |
55123
a389b50e6a42
no document for Cartouche_Examples: avoid problems typesetting "\001";
wenzelm
parents:
55075
diff
changeset
|
548 |
Cartouche_Examples |
48481 | 549 |
theories |
59090 | 550 |
Commands |
57507 | 551 |
Adhoc_Overloading_Examples |
48481 | 552 |
Iff_Oracle |
553 |
Coercion_Examples |
|
554 |
Abstract_NAT |
|
555 |
Guess |
|
62999 | 556 |
Functions |
48481 | 557 |
Induction_Schema |
558 |
LocaleTest2 |
|
559 |
Records |
|
560 |
While_Combinator_Example |
|
561 |
MonoidGroup |
|
562 |
BinEx |
|
563 |
Hex_Bin_Examples |
|
564 |
Antiquote |
|
565 |
Multiquote |
|
566 |
PER |
|
567 |
NatSum |
|
568 |
ThreeDivides |
|
59190
3a594fd13ca4
3 old example lemmas by Amine listed in the top 100 theorems
kleing
parents:
59162
diff
changeset
|
569 |
Cubic_Quartic |
59739 | 570 |
Pythagoras |
48481 | 571 |
Intuitionistic |
572 |
CTL |
|
573 |
Arith_Examples |
|
574 |
Tree23 |
|
58644 | 575 |
Bubblesort |
48481 | 576 |
MergeSort |
577 |
Lagrange |
|
578 |
Groebner_Examples |
|
579 |
Unification |
|
580 |
Primrec |
|
581 |
Tarski |
|
582 |
Classical |
|
583 |
Set_Theory |
|
584 |
Termination |
|
585 |
Coherent |
|
586 |
PresburgerEx |
|
51093 | 587 |
Reflection_Examples |
48481 | 588 |
Sqrt |
589 |
Sqrt_Script |
|
61368 | 590 |
Transfer_Debug |
48481 | 591 |
Transfer_Ex |
592 |
Transfer_Int_Nat |
|
56922 | 593 |
Transitive_Closure_Table_Ex |
48481 | 594 |
HarmonicSeries |
595 |
Refute_Examples |
|
596 |
Execute_Choice |
|
597 |
Gauge_Integration |
|
598 |
Dedekind_Real |
|
599 |
Quicksort |
|
600 |
Birthday_Paradox |
|
601 |
List_to_Set_Comprehension_Examples |
|
602 |
Seq |
|
603 |
Simproc_Tests |
|
604 |
Executable_Relation |
|
605 |
FinFunPred |
|
55663 | 606 |
Set_Comprehension_Pointfree_Examples |
48481 | 607 |
Parallel_Example |
50138 | 608 |
IArray_Examples |
53430 | 609 |
Simps_Case_Conv_Examples |
53935 | 610 |
ML |
59739 | 611 |
Rewrite_Examples |
56815 | 612 |
SAT_Examples |
58630 | 613 |
SOS |
58418 | 614 |
SOS_Cert |
60603
09ecbd791d4a
add examples from Freek's top 100 theorems (thms 30, 73, 77)
bulwahn
parents:
60470
diff
changeset
|
615 |
Ballot |
09ecbd791d4a
add examples from Freek's top 100 theorems (thms 30, 73, 77)
bulwahn
parents:
60470
diff
changeset
|
616 |
Erdoes_Szekeres |
09ecbd791d4a
add examples from Freek's top 100 theorems (thms 30, 73, 77)
bulwahn
parents:
60470
diff
changeset
|
617 |
Sum_of_Powers |
62285 | 618 |
Sudoku |
63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
63091
diff
changeset
|
619 |
Code_Timing |
63375
59803048b0e8
basic facts about almost everywhere fix bijections
haftmann
parents:
63283
diff
changeset
|
620 |
Perm_Fragments |
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
|
621 |
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
|
622 |
Meson_Test |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
623 |
document_files "root.bib" "root.tex" |
48481 | 624 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
625 |
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
|
626 |
description {* |
61935 | 627 |
Miscellaneous Isabelle/Isar examples. |
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
628 |
*} |
61939 | 629 |
options [quick_and_dirty] |
48481 | 630 |
theories [document = false] |
631 |
"~~/src/HOL/Library/Lattice_Syntax" |
|
632 |
"../Number_Theory/Primes" |
|
633 |
theories |
|
61939 | 634 |
Knaster_Tarski |
635 |
Peirce |
|
636 |
Drinker |
|
48481 | 637 |
Cantor |
61938 | 638 |
Schroeder_Bernstein |
61939 | 639 |
Structured_Statements |
640 |
Basic_Logic |
|
48481 | 641 |
Expr_Compiler |
642 |
Fibonacci |
|
643 |
Group |
|
644 |
Group_Context |
|
645 |
Group_Notepad |
|
646 |
Hoare_Ex |
|
647 |
Mutilated_Checkerboard |
|
648 |
Puzzle |
|
649 |
Summation |
|
61935 | 650 |
First_Order_Logic |
651 |
Higher_Order_Logic |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
652 |
document_files |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
653 |
"root.bib" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
654 |
"root.tex" |
48481 | 655 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
656 |
session "HOL-Eisbach" in Eisbach = HOL + |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
657 |
description {* |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
658 |
The Eisbach proof method language and "match" method. |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
659 |
*} |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
660 |
theories |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
661 |
Eisbach |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
662 |
Tests |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
663 |
Examples |
62168
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
62155
diff
changeset
|
664 |
Examples_FOL |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
60008
diff
changeset
|
665 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
666 |
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
|
667 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
668 |
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
|
669 |
*} |
48481 | 670 |
theories [document = false] "~~/src/HOL/Library/Nat_Bijection" |
671 |
theories SET_Protocol |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
672 |
document_files "root.tex" |
48481 | 673 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
674 |
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
|
675 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
676 |
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
|
677 |
*} |
48481 | 678 |
theories Cplex |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
679 |
document_files "root.tex" |
48481 | 680 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
681 |
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
|
682 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
683 |
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
|
684 |
*} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
685 |
options [document = false] |
48481 | 686 |
theories TLA |
687 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
688 |
session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
689 |
options [document = false] |
48481 | 690 |
theories Inc |
691 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
692 |
session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
693 |
options [document = false] |
48481 | 694 |
theories DBuffer |
695 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
696 |
session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
697 |
options [document = false] |
48481 | 698 |
theories MemoryImplementation |
699 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
700 |
session "HOL-TPTP" in TPTP = HOL + |
48481 | 701 |
description {* |
702 |
Author: Jasmin Blanchette, TU Muenchen |
|
703 |
Author: Nik Sultana, University of Cambridge |
|
704 |
Copyright 2011 |
|
705 |
||
706 |
TPTP-related extensions. |
|
707 |
*} |
|
62354 | 708 |
options [document = false] |
48481 | 709 |
theories |
710 |
ATP_Theory_Export |
|
711 |
MaSh_Eval |
|
712 |
TPTP_Interpret |
|
713 |
THF_Arith |
|
55596
928b9f677165
reconstruction framework for LEO-II's TPTP proofs;
sultana
parents:
55450
diff
changeset
|
714 |
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
|
715 |
theories |
48481 | 716 |
ATP_Problem_Import |
717 |
||
50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset
|
718 |
session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL + |
48481 | 719 |
theories |
720 |
Multivariate_Analysis |
|
721 |
Determinants |
|
56215 | 722 |
PolyRoots |
63078
e49dc94eb624
Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
paulson <lp15@cam.ac.uk>
parents:
63070
diff
changeset
|
723 |
Polytope |
56215 | 724 |
Complex_Analysis_Basics |
59741
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
725 |
Complex_Transcendental |
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60804
diff
changeset
|
726 |
Cauchy_Integral_Thm |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
727 |
document_files |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
728 |
"root.tex" |
48481 | 729 |
|
59922
1b6283aa7c94
rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
wenzelm
parents:
59903
diff
changeset
|
730 |
session "HOL-Multivariate_Analysis-ex" in "Multivariate_Analysis/ex" = "HOL-Multivariate_Analysis" + |
1b6283aa7c94
rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
wenzelm
parents:
59903
diff
changeset
|
731 |
theories |
1b6283aa7c94
rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
wenzelm
parents:
59903
diff
changeset
|
732 |
Approximations |
1b6283aa7c94
rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
wenzelm
parents:
59903
diff
changeset
|
733 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
734 |
session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" + |
48481 | 735 |
theories [document = false] |
736 |
"~~/src/HOL/Library/Countable" |
|
737 |
"~~/src/HOL/Library/Permutation" |
|
56994 | 738 |
"~~/src/HOL/Library/Order_Continuity" |
739 |
"~~/src/HOL/Library/Diagonal_Subsequence" |
|
48481 | 740 |
theories |
741 |
Probability |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
742 |
document_files "root.tex" |
48481 | 743 |
|
61946
844881193616
put example into separate session, to restrict precious session image to library theories
haftmann
parents:
61939
diff
changeset
|
744 |
session "HOL-Probability-ex" in "Probability/ex" = "HOL-Probability" + |
844881193616
put example into separate session, to restrict precious session image to library theories
haftmann
parents:
61939
diff
changeset
|
745 |
theories |
844881193616
put example into separate session, to restrict precious session image to library theories
haftmann
parents:
61939
diff
changeset
|
746 |
"Dining_Cryptographers" |
844881193616
put example into separate session, to restrict precious session image to library theories
haftmann
parents:
61939
diff
changeset
|
747 |
"Koepf_Duermuth_Countermeasure" |
844881193616
put example into separate session, to restrict precious session image to library theories
haftmann
parents:
61939
diff
changeset
|
748 |
"Measure_Not_CCC" |
844881193616
put example into separate session, to restrict precious session image to library theories
haftmann
parents:
61939
diff
changeset
|
749 |
|
59898
81c70bdbd908
clarified "main" group, e.g. relevant for Isabelle/jEdit menu;
wenzelm
parents:
59810
diff
changeset
|
750 |
session "HOL-Nominal" in Nominal = HOL + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
751 |
options [document = false] |
48481 | 752 |
theories Nominal |
753 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
754 |
session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" + |
62354 | 755 |
options [document = false] |
58329
a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents:
58313
diff
changeset
|
756 |
theories |
59162
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
757 |
Class3 |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
758 |
CK_Machine |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
759 |
Compile |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
760 |
Contexts |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
761 |
Crary |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
762 |
CR_Takahashi |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
763 |
CR |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
764 |
Fsub |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
765 |
Height |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
766 |
Lambda_mu |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
767 |
Lam_Funs |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
768 |
LocalWeakening |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
769 |
Pattern |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
770 |
SN |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
771 |
SOS |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
772 |
Standardization |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
773 |
Support |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
774 |
Type_Preservation |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
775 |
Weakening |
dca5594761f2
afford full test, with slightly improved scheduling order;
wenzelm
parents:
59144
diff
changeset
|
776 |
W |
58329
a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents:
58313
diff
changeset
|
777 |
theories [quick_and_dirty] |
a31404ec7414
run larger nominal examples only 'ISABELLE_FULL_TEST'
blanchet
parents:
58313
diff
changeset
|
778 |
VC_Condition |
48481 | 779 |
|
55054
e1f3714bc508
moved subset of 'HOL-Cardinals' needed for BNF into 'HOL'
blanchet
parents:
55033
diff
changeset
|
780 |
session "HOL-Cardinals" in Cardinals = HOL + |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
781 |
description {* |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
782 |
Ordinals and Cardinals, Full Theories. |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
783 |
*} |
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
|
784 |
options [document = false] |
59747 | 785 |
theories |
786 |
Cardinals |
|
787 |
Bounded_Set |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
788 |
document_files |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
789 |
"intro.tex" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
790 |
"root.tex" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
791 |
"root.bib" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
792 |
|
58309
a09ec6daaa19
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
blanchet
parents:
58308
diff
changeset
|
793 |
session "HOL-Datatype_Examples" in Datatype_Examples = HOL + |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
794 |
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
|
795 |
(Co)datatype Examples. |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
796 |
*} |
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
|
797 |
options [document = false] |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
798 |
theories |
56454 | 799 |
Compat |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
800 |
Lambda_Term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
801 |
Process |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
802 |
TreeFsetI |
49872 | 803 |
"Derivation_Trees/Gram_Lang" |
804 |
"Derivation_Trees/Parallel" |
|
50517 | 805 |
Koenig |
60921 | 806 |
Lift_BNF |
61745 | 807 |
Milner_Tofte |
54961 | 808 |
Stream_Processor |
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset
|
809 |
Misc_Codatatype |
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52726
diff
changeset
|
810 |
Misc_Datatype |
54193 | 811 |
Misc_Primcorec |
53306 | 812 |
Misc_Primrec |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
48932
diff
changeset
|
813 |
|
62694 | 814 |
session "HOL-Corec_Examples" in Corec_Examples = HOL + |
815 |
description {* |
|
816 |
Corecursion Examples. |
|
817 |
*} |
|
818 |
options [document = false] |
|
819 |
theories |
|
820 |
LFilter |
|
62734 | 821 |
Paper_Examples |
62694 | 822 |
Stream_Processor |
62696 | 823 |
"Tests/Simple_Nesting" |
824 |
theories [quick_and_dirty] |
|
825 |
"Tests/GPV_Bare_Bones" |
|
826 |
"Tests/Merge_D" |
|
827 |
"Tests/Merge_Poly" |
|
828 |
"Tests/Misc_Mono" |
|
829 |
"Tests/Misc_Poly" |
|
830 |
"Tests/Small_Concrete" |
|
62725 | 831 |
"Tests/Stream_Friends" |
62696 | 832 |
"Tests/TLList_Friends" |
63190 | 833 |
"Tests/Type_Class" |
62694 | 834 |
|
50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset
|
835 |
session "HOL-Word" (main) in Word = HOL + |
48481 | 836 |
theories Word |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
837 |
document_files "root.bib" "root.tex" |
48481 | 838 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
839 |
session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
840 |
options [document = false] |
48481 | 841 |
theories WordExamples |
842 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
843 |
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
|
844 |
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
|
845 |
StateSpaceEx |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
846 |
document_files "root.tex" |
48481 | 847 |
|
62479 | 848 |
session "HOL-Nonstandard_Analysis" in Nonstandard_Analysis = HOL + |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
849 |
description {* |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
850 |
Nonstandard analysis. |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
851 |
*} |
62479 | 852 |
theories |
853 |
Nonstandard_Analysis |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
854 |
document_files "root.tex" |
48481 | 855 |
|
62479 | 856 |
session "HOL-Nonstandard_Analysis-Examples" in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
857 |
options [document = false] |
48481 | 858 |
theories NSPrimes |
859 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
860 |
session "HOL-Mirabelle" in Mirabelle = HOL + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
861 |
options [document = false] |
48481 | 862 |
theories Mirabelle_Test |
48589
fb446a780d50
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
wenzelm
parents:
48588
diff
changeset
|
863 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
864 |
session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" + |
62354 | 865 |
options [document = false, 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
|
866 |
theories Ex |
48481 | 867 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
868 |
session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" + |
62354 | 869 |
options [document = false, quick_and_dirty] |
48481 | 870 |
theories |
52722 | 871 |
Boogie |
48481 | 872 |
SMT_Examples |
873 |
SMT_Word_Examples |
|
50666
6f48853f08d5
actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
blanchet
parents:
50665
diff
changeset
|
874 |
SMT_Tests |
48481 | 875 |
files |
58367
8af1e68d7e1a
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents:
58351
diff
changeset
|
876 |
"Boogie_Dijkstra.certs" |
8af1e68d7e1a
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents:
58351
diff
changeset
|
877 |
"Boogie_Max.certs" |
8af1e68d7e1a
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents:
58351
diff
changeset
|
878 |
"SMT_Examples.certs" |
8af1e68d7e1a
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents:
58351
diff
changeset
|
879 |
"SMT_Word_Examples.certs" |
8af1e68d7e1a
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
blanchet
parents:
58351
diff
changeset
|
880 |
"VCC_Max.certs" |
48481 | 881 |
|
50844
b95ff3744815
populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
wenzelm
parents:
50833
diff
changeset
|
882 |
session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
883 |
options [document = false] |
48481 | 884 |
theories SPARK |
885 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
886 |
session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" + |
59810
e749a0f2f401
HOL-SPARK .prv files are subject to system option spark_prv;
wenzelm
parents:
59777
diff
changeset
|
887 |
options [document = false, spark_prv = false] |
48481 | 888 |
theories |
889 |
"Gcd/Greatest_Common_Divisor" |
|
890 |
||
891 |
"Liseq/Longest_Increasing_Subsequence" |
|
892 |
||
893 |
"RIPEMD-160/F" |
|
894 |
"RIPEMD-160/Hash" |
|
895 |
"RIPEMD-160/K_L" |
|
896 |
"RIPEMD-160/K_R" |
|
897 |
"RIPEMD-160/R_L" |
|
898 |
"RIPEMD-160/Round" |
|
899 |
"RIPEMD-160/R_R" |
|
900 |
"RIPEMD-160/S_L" |
|
901 |
"RIPEMD-160/S_R" |
|
902 |
||
903 |
"Sqrt/Sqrt" |
|
904 |
files |
|
905 |
"Gcd/greatest_common_divisor/g_c_d.fdl" |
|
906 |
"Gcd/greatest_common_divisor/g_c_d.rls" |
|
907 |
"Gcd/greatest_common_divisor/g_c_d.siv" |
|
908 |
"Liseq/liseq/liseq_length.fdl" |
|
909 |
"Liseq/liseq/liseq_length.rls" |
|
910 |
"Liseq/liseq/liseq_length.siv" |
|
911 |
"RIPEMD-160/rmd/f.fdl" |
|
912 |
"RIPEMD-160/rmd/f.rls" |
|
913 |
"RIPEMD-160/rmd/f.siv" |
|
914 |
"RIPEMD-160/rmd/hash.fdl" |
|
915 |
"RIPEMD-160/rmd/hash.rls" |
|
916 |
"RIPEMD-160/rmd/hash.siv" |
|
917 |
"RIPEMD-160/rmd/k_l.fdl" |
|
918 |
"RIPEMD-160/rmd/k_l.rls" |
|
919 |
"RIPEMD-160/rmd/k_l.siv" |
|
920 |
"RIPEMD-160/rmd/k_r.fdl" |
|
921 |
"RIPEMD-160/rmd/k_r.rls" |
|
922 |
"RIPEMD-160/rmd/k_r.siv" |
|
923 |
"RIPEMD-160/rmd/r_l.fdl" |
|
924 |
"RIPEMD-160/rmd/r_l.rls" |
|
925 |
"RIPEMD-160/rmd/r_l.siv" |
|
926 |
"RIPEMD-160/rmd/round.fdl" |
|
927 |
"RIPEMD-160/rmd/round.rls" |
|
928 |
"RIPEMD-160/rmd/round.siv" |
|
929 |
"RIPEMD-160/rmd/r_r.fdl" |
|
930 |
"RIPEMD-160/rmd/r_r.rls" |
|
931 |
"RIPEMD-160/rmd/r_r.siv" |
|
932 |
"RIPEMD-160/rmd/s_l.fdl" |
|
933 |
"RIPEMD-160/rmd/s_l.rls" |
|
934 |
"RIPEMD-160/rmd/s_l.siv" |
|
935 |
"RIPEMD-160/rmd/s_r.fdl" |
|
936 |
"RIPEMD-160/rmd/s_r.rls" |
|
937 |
"RIPEMD-160/rmd/s_r.siv" |
|
938 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
939 |
session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" + |
59810
e749a0f2f401
HOL-SPARK .prv files are subject to system option spark_prv;
wenzelm
parents:
59777
diff
changeset
|
940 |
options [show_question_marks = false, spark_prv = false] |
48481 | 941 |
theories |
942 |
Example_Verification |
|
943 |
VC_Principles |
|
944 |
Reference |
|
945 |
Complex_Types |
|
946 |
files |
|
947 |
"complex_types_app/initialize.fdl" |
|
948 |
"complex_types_app/initialize.rls" |
|
949 |
"complex_types_app/initialize.siv" |
|
950 |
"loop_invariant/proc1.fdl" |
|
951 |
"loop_invariant/proc1.rls" |
|
952 |
"loop_invariant/proc1.siv" |
|
953 |
"loop_invariant/proc2.fdl" |
|
954 |
"loop_invariant/proc2.rls" |
|
955 |
"loop_invariant/proc2.siv" |
|
956 |
"simple_greatest_common_divisor/g_c_d.fdl" |
|
957 |
"simple_greatest_common_divisor/g_c_d.rls" |
|
958 |
"simple_greatest_common_divisor/g_c_d.siv" |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
959 |
document_files |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
960 |
"complex_types.ads" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
961 |
"complex_types_app.adb" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
962 |
"complex_types_app.ads" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
963 |
"Gcd.adb" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
964 |
"Gcd.ads" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
965 |
"intro.tex" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
966 |
"loop_invariant.adb" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
967 |
"loop_invariant.ads" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
968 |
"root.bib" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
969 |
"root.tex" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
970 |
"Simple_Gcd.adb" |
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
971 |
"Simple_Gcd.ads" |
48481 | 972 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
973 |
session "HOL-Mutabelle" in Mutabelle = HOL + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
974 |
options [document = false] |
48481 | 975 |
theories MutabelleExtra |
976 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
977 |
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
|
978 |
options [document = false] |
48588 | 979 |
theories |
48690 | 980 |
Quickcheck_Examples |
981 |
Quickcheck_Lattice_Examples |
|
982 |
Completeness |
|
983 |
Quickcheck_Interfaces |
|
57584
155b7e3b729e
proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
wenzelm
parents:
57544
diff
changeset
|
984 |
theories [condition = ISABELLE_GHC] |
57544
8840fa17e17c
reactivate session Quickcheck_Examples
Andreas Lochbihler
parents:
57543
diff
changeset
|
985 |
Hotel_Example |
48598 | 986 |
Quickcheck_Narrowing_Examples |
48588 | 987 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
988 |
session "HOL-Quotient_Examples" in Quotient_Examples = HOL + |
48481 | 989 |
description {* |
990 |
Author: Cezary Kaliszyk and Christian Urban |
|
991 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
992 |
options [document = false] |
48481 | 993 |
theories |
994 |
DList |
|
995 |
FSet |
|
996 |
Quotient_Int |
|
997 |
Quotient_Message |
|
998 |
Lift_FSet |
|
999 |
Lift_Set |
|
1000 |
Lift_Fun |
|
1001 |
Quotient_Rat |
|
1002 |
Lift_DList |
|
53682
1b55aeda0e46
include Int_Pow into Quotient_Examples; add end of the theory
kuncar
parents:
53430
diff
changeset
|
1003 |
Int_Pow |
60237 | 1004 |
Lifting_Code_Dt_Test |
48481 | 1005 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1006 |
session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1007 |
options [document = false] |
62354 | 1008 |
theories |
48481 | 1009 |
Examples |
1010 |
Predicate_Compile_Tests |
|
61140
78ece168f5b5
reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents:
60921
diff
changeset
|
1011 |
Predicate_Compile_Quickcheck_Examples |
48481 | 1012 |
Specialisation_Examples |
48690 | 1013 |
IMP_1 |
1014 |
IMP_2 |
|
55450
9eddc17749f7
reactivate some examples that still appear to work;
wenzelm
parents:
55447
diff
changeset
|
1015 |
(* FIXME since 21-Jul-2011 |
61140
78ece168f5b5
reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents:
60921
diff
changeset
|
1016 |
Hotel_Example_Small_Generator *) |
48690 | 1017 |
IMP_3 |
61140
78ece168f5b5
reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents:
60921
diff
changeset
|
1018 |
IMP_4 |
62242
a4e6ea45f416
guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents:
62168
diff
changeset
|
1019 |
theories [condition = ISABELLE_SWIPL] |
48690 | 1020 |
Code_Prolog_Examples |
1021 |
Context_Free_Grammar_Example |
|
1022 |
Hotel_Example_Prolog |
|
1023 |
Lambda_Example |
|
1024 |
List_Examples |
|
62242
a4e6ea45f416
guard sessions that no longer work with SML/NJ -- memory problems;
wenzelm
parents:
62168
diff
changeset
|
1025 |
theories [condition = ISABELLE_SWIPL, quick_and_dirty] |
48690 | 1026 |
Reg_Exp_Example |
48481 | 1027 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1028 |
session HOLCF (main) in HOLCF = HOL + |
48338 | 1029 |
description {* |
1030 |
Author: Franz Regensburger |
|
1031 |
Author: Brian Huffman |
|
1032 |
||
1033 |
HOLCF -- a semantic extension of HOL by the LCF logic. |
|
1034 |
*} |
|
48470
7483aa690b4f
clarified "document" again, eliminated redundant "no_document";
wenzelm
parents:
48458
diff
changeset
|
1035 |
theories [document = false] |
48338 | 1036 |
"~~/src/HOL/Library/Nat_Bijection" |
1037 |
"~~/src/HOL/Library/Countable" |
|
48481 | 1038 |
theories |
1039 |
Plain_HOLCF |
|
1040 |
Fixrec |
|
1041 |
HOLCF |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
1042 |
document_files "root.tex" |
48481 | 1043 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1044 |
session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF + |
48481 | 1045 |
theories |
1046 |
Domain_ex |
|
1047 |
Fixrec_ex |
|
1048 |
New_Domain |
|
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
1049 |
document_files "root.tex" |
48481 | 1050 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1051 |
session "HOLCF-Library" in "HOLCF/Library" = HOLCF + |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1052 |
options [document = false] |
48481 | 1053 |
theories HOLCF_Library |
1054 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1055 |
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
|
1056 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1057 |
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
|
1058 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1059 |
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
|
1060 |
*} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1061 |
options [document = false] |
48481 | 1062 |
theories HoareEx |
56781
f2eb0f22589f
systematic replacement of 'files' by 'document_files';
wenzelm
parents:
56680
diff
changeset
|
1063 |
document_files "root.tex" |
48338 | 1064 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1065 |
session "HOLCF-ex" in "HOLCF/ex" = HOLCF + |
51421
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
1066 |
description {* |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
1067 |
Miscellaneous examples for HOLCF. |
b5d559b101d9
more uniform session descriptions, which show up in chapter index;
wenzelm
parents:
51403
diff
changeset
|
1068 |
*} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1069 |
options [document = false] |
48481 | 1070 |
theories |
1071 |
Dnat |
|
1072 |
Dagstuhl |
|
1073 |
Focus_ex |
|
1074 |
Fix2 |
|
1075 |
Hoare |
|
1076 |
Concurrency_Monad |
|
1077 |
Loop |
|
1078 |
Powerdomain_ex |
|
1079 |
Domain_Proofs |
|
1080 |
Letrec |
|
1081 |
Pattern_Match |
|
1082 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1083 |
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
|
1084 |
description {* |
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1085 |
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
|
1086 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1087 |
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
|
1088 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1089 |
"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
|
1090 |
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
|
1091 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1092 |
"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
|
1093 |
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
|
1094 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1095 |
"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
|
1096 |
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
|
1097 |
*} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1098 |
options [document = false] |
48481 | 1099 |
theories |
1100 |
Fstreams |
|
1101 |
FOCUS |
|
1102 |
Buffer_adm |
|
1103 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1104 |
session IOA in "HOLCF/IOA" = HOLCF + |
48481 | 1105 |
description {* |
1106 |
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
|
1107 |
Copyright 1997 TU München |
48481 | 1108 |
|
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1109 |
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
|
1110 |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
1111 |
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
|
1112 |
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
|
1113 |
finite and infinite sequences. |
48481 | 1114 |
*} |
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1115 |
options [document = false] |
62008 | 1116 |
theories "Abstraction" |
48481 | 1117 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1118 |
session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA + |
48481 | 1119 |
description {* |
1120 |
Author: Olaf Mueller |
|
1121 |
||
1122 |
The Alternating Bit Protocol performed in I/O-Automata. |
|
1123 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1124 |
options [document = false] |
59503 | 1125 |
theories |
1126 |
Correctness |
|
1127 |
Spec |
|
48481 | 1128 |
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1129 |
session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA + |
48481 | 1130 |
description {* |
1131 |
Author: Tobias Nipkow & Konrad Slind |
|
1132 |
||
1133 |
A network transmission protocol, performed in the |
|
1134 |
I/O automata formalization by Olaf Mueller. |
|
1135 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1136 |
options [document = false] |
48481 | 1137 |
theories Correctness |
1138 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1139 |
session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA + |
48481 | 1140 |
description {* |
1141 |
Author: Olaf Mueller |
|
1142 |
||
1143 |
Memory storage case study. |
|
1144 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1145 |
options [document = false] |
48481 | 1146 |
theories Correctness |
1147 |
||
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48721
diff
changeset
|
1148 |
session "IOA-ex" in "HOLCF/IOA/ex" = IOA + |
48481 | 1149 |
description {* |
1150 |
Author: Olaf Mueller |
|
1151 |
*} |
|
48483
9bfb6978eb80
more explicit document = false to reduce warnings;
wenzelm
parents:
48481
diff
changeset
|
1152 |
options [document = false] |
48481 | 1153 |
theories |
1154 |
TrivEx |
|
1155 |
TrivEx2 |