| author | blanchet |
| Thu, 26 Jul 2012 10:48:03 +0200 | |
| changeset 48530 | d443166f9520 |
| parent 48502 | fd03877ad5bc |
| child 48509 | 4854ced3e9d7 |
| permissions | -rw-r--r-- |
|
48502
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
1 |
session Classes! in "Classes/Thy" = HOL + |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
2 |
options [browser_info = false, document = false, document_dump = document, document_dump_only] |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
3 |
theories [document = false] Setup |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
4 |
theories Classes |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
5 |
|
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
6 |
session Codegen! in "Codegen/Thy" = "HOL-Library" + |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
7 |
options [browser_info = false, document = false, document_dump = document, document_dump_only, |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
8 |
print_mode = "no_brackets,iff"] |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
9 |
theories [document = false] Setup |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
10 |
theories |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
11 |
Introduction |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
12 |
Foundations |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
13 |
Refinement |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
14 |
Inductive_Predicate |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
15 |
Evaluation |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
16 |
Adaptation |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
17 |
Further |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
18 |
|
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
19 |
session Functions! in "Functions/Thy" = HOL + |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
20 |
options [browser_info = false, document = false, document_dump = document, document_dump_only] |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
21 |
theories Functions |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
22 |
|
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
23 |
session IsarImplementation! in "IsarImplementation/Thy" = HOL + |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
24 |
options [browser_info = false, document = false, document_dump = document, document_dump_only] |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
25 |
theories |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
26 |
Eq |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
27 |
Integration |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
28 |
Isar |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
29 |
Local_Theory |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
30 |
Logic |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
31 |
ML |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
32 |
Prelim |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
33 |
Proof |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
34 |
Syntax |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
35 |
Tactic |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
36 |
|
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
37 |
session IsarRef in "IsarRef/Thy" = HOL + |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
38 |
options [browser_info = false, document = false, document_dump = document, document_dump_only, |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
39 |
quick_and_dirty] |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
40 |
theories |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
41 |
Preface |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
42 |
Synopsis |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
43 |
Framework |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
44 |
First_Order_Logic |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
45 |
Outer_Syntax |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
46 |
Document_Preparation |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
47 |
Spec |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
48 |
Proof |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
49 |
Inner_Syntax |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
50 |
Misc |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
51 |
Generic |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
52 |
HOL_Specific |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
53 |
Quick_Reference |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
54 |
Symbols |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
55 |
ML_Tactic |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
56 |
|
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
57 |
session IsarRef in "IsarRef/Thy" = HOLCF + |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
58 |
options [browser_info = false, document = false, document_dump = document, document_dump_only, |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
59 |
quick_and_dirty] |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
60 |
theories HOLCF_Specific |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
61 |
|
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
62 |
session IsarRef in "IsarRef/Thy" = ZF + |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
63 |
options [browser_info = false, document = false, document_dump = document, document_dump_only, |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
64 |
quick_and_dirty] |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
65 |
theories ZF_Specific |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
66 |
|
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
67 |
session LaTeXsugar! in "LaTeXsugar/Sugar" = HOL + |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
68 |
options [browser_info = false, document = false, document_dump = document, document_dump_only, |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
69 |
threads = 1] (* FIXME *) |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
70 |
theories [document_dump = ""] |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
71 |
"~~/src/HOL/Library/LaTeXsugar" |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
72 |
"~~/src/HOL/Library/OptionalSugar" |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
73 |
theories Sugar |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
74 |
|
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
75 |
session Locales! in "Locales/Locales" = HOL + |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
76 |
options [browser_info = false, document = false, document_dump = document, document_dump_only] |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
77 |
theories |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
78 |
Examples1 |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
79 |
Examples2 |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
80 |
Examples3 |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
81 |
|
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
82 |
session Main! in "Main/Docs" = HOL + |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
83 |
options [browser_info = false, document = false, document_dump = document, document_dump_only] |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
84 |
theories Main_Doc |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
85 |
|
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
86 |
session ProgProve! in "ProgProve/Thys" = HOL + |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
87 |
options [browser_info = false, document = false, document_dump = document, document_dump_only, |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
88 |
show_question_marks = false] |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
89 |
theories |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
90 |
Basics |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
91 |
Bool_nat_list |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
92 |
MyList |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
93 |
Types_and_funs |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
94 |
Logic |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
95 |
Isar |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
96 |
|
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
97 |
session System! in "System/Thy" = Pure + |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
98 |
options [browser_info = false, document = false, document_dump = document, document_dump_only] |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
99 |
theories |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
100 |
Basics |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
101 |
Interfaces |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
102 |
Scala |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
103 |
Presentation |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
104 |
Misc |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
105 |
|
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
106 |
(* session Tutorial in "Tutorial" = HOL + FIXME *) |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
107 |
|
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
108 |
session examples in "ZF" = ZF + |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
109 |
options [browser_info = false, document = false, document_dump = document, document_dump_only, |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
110 |
print_mode = "brackets"] |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
111 |
theories |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
112 |
IFOL_examples |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
113 |
FOL_examples |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
114 |
ZF_examples |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
115 |
If |
|
fd03877ad5bc
session specifications for doc-src, excluding TutorialI for now;
wenzelm
parents:
diff
changeset
|
116 |