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