|
wenzelm@49524
|
1 |
session Classes! (doc) in "Classes/Thy" = HOL +
|
|
wenzelm@49531
|
2 |
options [browser_info = false, document = false,
|
|
wenzelm@49531
|
3 |
document_dump = document, document_dump_mode = "tex"]
|
|
wenzelm@49517
|
4 |
theories [document = false] Setup
|
|
wenzelm@49517
|
5 |
theories Classes
|
|
wenzelm@49517
|
6 |
|
|
wenzelm@49524
|
7 |
session Codegen! (doc) in "Codegen/Thy" = "HOL-Library" +
|
|
wenzelm@49531
|
8 |
options [browser_info = false, document = false,
|
|
wenzelm@49531
|
9 |
document_dump = document, document_dump_mode = "tex",
|
|
wenzelm@49517
|
10 |
print_mode = "no_brackets,iff"]
|
|
wenzelm@49517
|
11 |
theories [document = false] Setup
|
|
wenzelm@49517
|
12 |
theories
|
|
wenzelm@49517
|
13 |
Introduction
|
|
wenzelm@49517
|
14 |
Foundations
|
|
wenzelm@49517
|
15 |
Refinement
|
|
wenzelm@49517
|
16 |
Inductive_Predicate
|
|
wenzelm@49517
|
17 |
Evaluation
|
|
wenzelm@49517
|
18 |
Adaptation
|
|
wenzelm@49517
|
19 |
Further
|
|
wenzelm@49517
|
20 |
|
|
wenzelm@49524
|
21 |
session Functions! (doc) in "Functions/Thy" = HOL +
|
|
wenzelm@49531
|
22 |
options [browser_info = false, document = false,
|
|
wenzelm@49531
|
23 |
document_dump = document, document_dump_mode = "tex"]
|
|
wenzelm@49517
|
24 |
theories Functions
|
|
wenzelm@49517
|
25 |
|
|
wenzelm@49524
|
26 |
session IsarImplementation! (doc) in "IsarImplementation/Thy" = HOL +
|
|
wenzelm@49531
|
27 |
options [browser_info = false, document = false,
|
|
wenzelm@49531
|
28 |
document_dump = document, document_dump_mode = "tex"]
|
|
wenzelm@49517
|
29 |
theories
|
|
wenzelm@49517
|
30 |
Eq
|
|
wenzelm@49517
|
31 |
Integration
|
|
wenzelm@49517
|
32 |
Isar
|
|
wenzelm@49517
|
33 |
Local_Theory
|
|
wenzelm@49517
|
34 |
Logic
|
|
wenzelm@49517
|
35 |
ML
|
|
wenzelm@49517
|
36 |
Prelim
|
|
wenzelm@49517
|
37 |
Proof
|
|
wenzelm@49517
|
38 |
Syntax
|
|
wenzelm@49517
|
39 |
Tactic
|
|
wenzelm@49517
|
40 |
|
|
wenzelm@49524
|
41 |
session IsarRef (doc) in "IsarRef/Thy" = HOL +
|
|
wenzelm@49531
|
42 |
options [browser_info = false, document = false,
|
|
wenzelm@49531
|
43 |
document_dump = document, document_dump_mode = "tex",
|
|
wenzelm@49517
|
44 |
quick_and_dirty]
|
|
wenzelm@49517
|
45 |
theories
|
|
wenzelm@49517
|
46 |
Preface
|
|
wenzelm@49517
|
47 |
Synopsis
|
|
wenzelm@49517
|
48 |
Framework
|
|
wenzelm@49517
|
49 |
First_Order_Logic
|
|
wenzelm@49517
|
50 |
Outer_Syntax
|
|
wenzelm@49517
|
51 |
Document_Preparation
|
|
wenzelm@49517
|
52 |
Spec
|
|
wenzelm@49517
|
53 |
Proof
|
|
wenzelm@49517
|
54 |
Inner_Syntax
|
|
wenzelm@49517
|
55 |
Misc
|
|
wenzelm@49517
|
56 |
Generic
|
|
wenzelm@49517
|
57 |
HOL_Specific
|
|
wenzelm@49517
|
58 |
Quick_Reference
|
|
wenzelm@49517
|
59 |
Symbols
|
|
wenzelm@49517
|
60 |
ML_Tactic
|
|
wenzelm@49517
|
61 |
|
|
wenzelm@49524
|
62 |
session IsarRef (doc) in "IsarRef/Thy" = HOLCF +
|
|
wenzelm@49531
|
63 |
options [browser_info = false, document = false,
|
|
wenzelm@49531
|
64 |
document_dump = document, document_dump_mode = "tex",
|
|
wenzelm@49517
|
65 |
quick_and_dirty]
|
|
wenzelm@49517
|
66 |
theories HOLCF_Specific
|
|
wenzelm@49517
|
67 |
|
|
wenzelm@49524
|
68 |
session IsarRef (doc) in "IsarRef/Thy" = ZF +
|
|
wenzelm@49531
|
69 |
options [browser_info = false, document = false,
|
|
wenzelm@49531
|
70 |
document_dump = document, document_dump_mode = "tex",
|
|
wenzelm@49517
|
71 |
quick_and_dirty]
|
|
wenzelm@49517
|
72 |
theories ZF_Specific
|
|
wenzelm@49517
|
73 |
|
|
wenzelm@49524
|
74 |
session LaTeXsugar! (doc) in "LaTeXsugar/Sugar" = HOL +
|
|
wenzelm@49531
|
75 |
options [browser_info = false, document = false,
|
|
wenzelm@49531
|
76 |
document_dump = document, document_dump_mode = "tex",
|
|
wenzelm@49517
|
77 |
threads = 1] (* FIXME *)
|
|
wenzelm@49517
|
78 |
theories [document_dump = ""]
|
|
wenzelm@49517
|
79 |
"~~/src/HOL/Library/LaTeXsugar"
|
|
wenzelm@49517
|
80 |
"~~/src/HOL/Library/OptionalSugar"
|
|
wenzelm@49517
|
81 |
theories Sugar
|
|
wenzelm@49517
|
82 |
|
|
wenzelm@49524
|
83 |
session Locales! (doc) in "Locales/Locales" = HOL +
|
|
wenzelm@49531
|
84 |
options [browser_info = false, document = false,
|
|
wenzelm@49531
|
85 |
document_dump = document, document_dump_mode = "tex"]
|
|
wenzelm@49517
|
86 |
theories
|
|
wenzelm@49517
|
87 |
Examples1
|
|
wenzelm@49517
|
88 |
Examples2
|
|
wenzelm@49517
|
89 |
Examples3
|
|
wenzelm@49517
|
90 |
|
|
wenzelm@49524
|
91 |
session Main! (doc) in "Main/Docs" = HOL +
|
|
wenzelm@49531
|
92 |
options [browser_info = false, document = false,
|
|
wenzelm@49531
|
93 |
document_dump = document, document_dump_mode = "tex"]
|
|
wenzelm@49517
|
94 |
theories Main_Doc
|
|
wenzelm@49517
|
95 |
|
|
wenzelm@49524
|
96 |
session ProgProve! (doc) in "ProgProve/Thys" = HOL +
|
|
wenzelm@49531
|
97 |
options [browser_info = false, document = false,
|
|
wenzelm@49531
|
98 |
document_dump = document, document_dump_mode = "tex",
|
|
wenzelm@49517
|
99 |
show_question_marks = false]
|
|
wenzelm@49517
|
100 |
theories
|
|
wenzelm@49517
|
101 |
Basics
|
|
wenzelm@49517
|
102 |
Bool_nat_list
|
|
wenzelm@49517
|
103 |
MyList
|
|
wenzelm@49517
|
104 |
Types_and_funs
|
|
wenzelm@49517
|
105 |
Logic
|
|
wenzelm@49517
|
106 |
Isar
|
|
wenzelm@49517
|
107 |
|
|
wenzelm@49524
|
108 |
session System! (doc) in "System/Thy" = Pure +
|
|
wenzelm@49531
|
109 |
options [browser_info = false, document = false,
|
|
wenzelm@49531
|
110 |
document_dump = document, document_dump_mode = "tex"]
|
|
wenzelm@49517
|
111 |
theories
|
|
wenzelm@49517
|
112 |
Basics
|
|
wenzelm@49517
|
113 |
Interfaces
|
|
wenzelm@49517
|
114 |
Scala
|
|
wenzelm@49517
|
115 |
Presentation
|
|
wenzelm@49517
|
116 |
Misc
|
|
wenzelm@49517
|
117 |
|
|
wenzelm@49541
|
118 |
session Tutorial (doc) in "TutorialI" = HOL +
|
|
wenzelm@49541
|
119 |
options [browser_info = false, document = false,
|
|
wenzelm@49541
|
120 |
document_dump = document, document_dump_mode = "tex",
|
|
wenzelm@49541
|
121 |
print_mode = "brackets", threads = 1 (* FIXME *)]
|
|
wenzelm@49541
|
122 |
theories [thy_output_indent = 5]
|
|
wenzelm@49541
|
123 |
"ToyList/ToyList"
|
|
wenzelm@49541
|
124 |
"Ifexpr/Ifexpr"
|
|
wenzelm@49541
|
125 |
"CodeGen/CodeGen"
|
|
wenzelm@49541
|
126 |
"Trie/Trie"
|
|
wenzelm@49541
|
127 |
"Datatype/ABexpr"
|
|
wenzelm@49541
|
128 |
"Datatype/unfoldnested"
|
|
wenzelm@49541
|
129 |
"Datatype/Nested"
|
|
wenzelm@49541
|
130 |
"Datatype/Fundata"
|
|
wenzelm@49541
|
131 |
"Fun/fun0"
|
|
wenzelm@49541
|
132 |
"Advanced/simp2"
|
|
wenzelm@49541
|
133 |
"CTL/PDL"
|
|
wenzelm@49541
|
134 |
"CTL/CTL"
|
|
wenzelm@49541
|
135 |
"CTL/CTLind"
|
|
wenzelm@49541
|
136 |
"Inductive/Even"
|
|
wenzelm@49541
|
137 |
"Inductive/Mutual"
|
|
wenzelm@49541
|
138 |
"Inductive/Star"
|
|
wenzelm@49541
|
139 |
"Inductive/AB"
|
|
wenzelm@49541
|
140 |
"Inductive/Advanced"
|
|
wenzelm@49541
|
141 |
"Misc/Tree"
|
|
wenzelm@49541
|
142 |
"Misc/Tree2"
|
|
wenzelm@49541
|
143 |
"Misc/Plus"
|
|
wenzelm@49541
|
144 |
"Misc/case_exprs"
|
|
wenzelm@49541
|
145 |
"Misc/fakenat"
|
|
wenzelm@49541
|
146 |
"Misc/natsum"
|
|
wenzelm@49541
|
147 |
"Misc/pairs2"
|
|
wenzelm@49541
|
148 |
"Misc/Option2"
|
|
wenzelm@49541
|
149 |
"Misc/types"
|
|
wenzelm@49541
|
150 |
"Misc/prime_def"
|
|
wenzelm@49541
|
151 |
"Misc/simp"
|
|
wenzelm@49541
|
152 |
"Misc/Itrev"
|
|
wenzelm@49541
|
153 |
"Misc/AdvancedInd"
|
|
wenzelm@49541
|
154 |
"Misc/appendix"
|
|
wenzelm@49541
|
155 |
theories
|
|
wenzelm@49541
|
156 |
"Protocol/NS_Public"
|
|
wenzelm@49541
|
157 |
"Documents/Documents"
|
|
wenzelm@49541
|
158 |
theories [document_dump = ""]
|
|
wenzelm@49541
|
159 |
"Types/Setup"
|
|
wenzelm@49541
|
160 |
theories
|
|
wenzelm@49541
|
161 |
"Types/Numbers"
|
|
wenzelm@49541
|
162 |
"Types/Pairs"
|
|
wenzelm@49541
|
163 |
"Types/Records"
|
|
wenzelm@49541
|
164 |
"Types/Typedefs"
|
|
wenzelm@49541
|
165 |
"Types/Overloading"
|
|
wenzelm@49541
|
166 |
"Types/Axioms"
|
|
wenzelm@49541
|
167 |
"Rules/Basic"
|
|
wenzelm@49541
|
168 |
"Rules/Blast"
|
|
wenzelm@49541
|
169 |
"Rules/Force"
|
|
wenzelm@49541
|
170 |
"Rules/Forward"
|
|
wenzelm@49541
|
171 |
"Rules/Tacticals"
|
|
wenzelm@49541
|
172 |
"Rules/find2"
|
|
wenzelm@49541
|
173 |
"Sets/Examples"
|
|
wenzelm@49541
|
174 |
"Sets/Functions"
|
|
wenzelm@49541
|
175 |
"Sets/Relations"
|
|
wenzelm@49541
|
176 |
"Sets/Recur"
|
|
wenzelm@49517
|
177 |
|
|
wenzelm@49524
|
178 |
session examples (doc) in "ZF" = ZF +
|
|
wenzelm@49531
|
179 |
options [browser_info = false, document = false,
|
|
wenzelm@49531
|
180 |
document_dump = document, document_dump_mode = "tex",
|
|
wenzelm@49517
|
181 |
print_mode = "brackets"]
|
|
wenzelm@49517
|
182 |
theories
|
|
wenzelm@49517
|
183 |
IFOL_examples
|
|
wenzelm@49517
|
184 |
FOL_examples
|
|
wenzelm@49517
|
185 |
ZF_examples
|
|
wenzelm@49517
|
186 |
If
|
|
wenzelm@49517
|
187 |
|