author  haftmann 
Sat, 05 Apr 2014 11:37:00 +0200  
changeset 56420  b266e7a86485 
parent 55385  169e12bbf9a3 
child 56451  856492b0f755 
permissions  rwrr 
51397
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
50426
diff
changeset

1 
chapter Doc 
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
50426
diff
changeset

2 

48950
9965099f51ad
more standard document preparation within session context;
wenzelm
parents:
48949
diff
changeset

3 
session Classes (doc) in "Classes" = HOL + 
55385
169e12bbf9a3
discontinued axiomatic 'classes', 'classrel', 'arities';
wenzelm
parents:
55159
diff
changeset

4 
options [document_variants = "classes", quick_and_dirty] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

5 
theories [document = false] Setup 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

6 
theories Classes 
48950
9965099f51ad
more standard document preparation within session context;
wenzelm
parents:
48949
diff
changeset

7 
files 
48971  8 
"../prepare_document" 
48956  9 
"../pdfsetup.sty" 
49318
612a04e7c853
some attempts to synchronize ROOT/files and document/build;
wenzelm
parents:
48985
diff
changeset

10 
"../iman.sty" 
612a04e7c853
some attempts to synchronize ROOT/files and document/build;
wenzelm
parents:
48985
diff
changeset

11 
"../extra.sty" 
612a04e7c853
some attempts to synchronize ROOT/files and document/build;
wenzelm
parents:
48985
diff
changeset

12 
"../isar.sty" 
612a04e7c853
some attempts to synchronize ROOT/files and document/build;
wenzelm
parents:
48985
diff
changeset

13 
"../manual.bib" 
48950
9965099f51ad
more standard document preparation within session context;
wenzelm
parents:
48949
diff
changeset

14 
"document/build" 
9965099f51ad
more standard document preparation within session context;
wenzelm
parents:
48949
diff
changeset

15 
"document/root.tex" 
9965099f51ad
more standard document preparation within session context;
wenzelm
parents:
48949
diff
changeset

16 
"document/style.sty" 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

17 

48951
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
48950
diff
changeset

18 
session Codegen (doc) in "Codegen" = "HOLLibrary" + 
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
48950
diff
changeset

19 
options [document_variants = "codegen", print_mode = "no_brackets,iff"] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

20 
theories [document = false] Setup 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

21 
theories 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

22 
Introduction 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

23 
Foundations 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

24 
Refinement 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

25 
Inductive_Predicate 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

26 
Evaluation 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

27 
Adaptation 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

28 
Further 
48951
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
48950
diff
changeset

29 
files 
48971  30 
"../prepare_document" 
48956  31 
"../pdfsetup.sty" 
49318
612a04e7c853
some attempts to synchronize ROOT/files and document/build;
wenzelm
parents:
48985
diff
changeset

32 
"../iman.sty" 
612a04e7c853
some attempts to synchronize ROOT/files and document/build;
wenzelm
parents:
48985
diff
changeset

33 
"../extra.sty" 
612a04e7c853
some attempts to synchronize ROOT/files and document/build;
wenzelm
parents:
48985
diff
changeset

34 
"../isar.sty" 
612a04e7c853
some attempts to synchronize ROOT/files and document/build;
wenzelm
parents:
48985
diff
changeset

35 
"../manual.bib" 
48951
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
48950
diff
changeset

36 
"document/build" 
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
48950
diff
changeset

37 
"document/root.tex" 
b9238cbcdd41
more standard document preparation within session context;
wenzelm
parents:
48950
diff
changeset

38 
"document/style.sty" 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

39 

55073  40 
session Datatypes (doc) in "Datatypes" = HOL + 
53618  41 
options [document_variants = "datatypes"] 
52822  42 
theories [document = false] Setup 
52792
3e651be14fcd
sketched documentation for new (co)datatype package
blanchet
parents:
52742
diff
changeset

43 
theories Datatypes 
3e651be14fcd
sketched documentation for new (co)datatype package
blanchet
parents:
52742
diff
changeset

44 
files 
3e651be14fcd
sketched documentation for new (co)datatype package
blanchet
parents:
52742
diff
changeset

45 
"../prepare_document" 
3e651be14fcd
sketched documentation for new (co)datatype package
blanchet
parents:
52742
diff
changeset

46 
"../pdfsetup.sty" 
3e651be14fcd
sketched documentation for new (co)datatype package
blanchet
parents:
52742
diff
changeset

47 
"../iman.sty" 
3e651be14fcd
sketched documentation for new (co)datatype package
blanchet
parents:
52742
diff
changeset

48 
"../extra.sty" 
3e651be14fcd
sketched documentation for new (co)datatype package
blanchet
parents:
52742
diff
changeset

49 
"../isar.sty" 
3e651be14fcd
sketched documentation for new (co)datatype package
blanchet
parents:
52742
diff
changeset

50 
"../manual.bib" 
3e651be14fcd
sketched documentation for new (co)datatype package
blanchet
parents:
52742
diff
changeset

51 
"document/build" 
3e651be14fcd
sketched documentation for new (co)datatype package
blanchet
parents:
52742
diff
changeset

52 
"document/root.tex" 
3e651be14fcd
sketched documentation for new (co)datatype package
blanchet
parents:
52742
diff
changeset

53 
"document/style.sty" 
3e651be14fcd
sketched documentation for new (co)datatype package
blanchet
parents:
52742
diff
changeset

54 

48948
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
48947
diff
changeset

55 
session Functions (doc) in "Functions" = HOL + 
54017
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53769
diff
changeset

56 
options [document_variants = "functions", skip_proofs = false, quick_and_dirty] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

57 
theories Functions 
48948
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
48947
diff
changeset

58 
files 
48971  59 
"../prepare_document" 
48956  60 
"../pdfsetup.sty" 
48948
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
48947
diff
changeset

61 
"../iman.sty" 
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
48947
diff
changeset

62 
"../extra.sty" 
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
48947
diff
changeset

63 
"../isar.sty" 
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
48947
diff
changeset

64 
"../manual.bib" 
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
48947
diff
changeset

65 
"document/build" 
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
48947
diff
changeset

66 
"document/conclusion.tex" 
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
48947
diff
changeset

67 
"document/intro.tex" 
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
48947
diff
changeset

68 
"document/mathpartir.sty" 
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
48947
diff
changeset

69 
"document/root.tex" 
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
48947
diff
changeset

70 
"document/style.sty" 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

71 

48969  72 
session Intro (doc) in "Intro" = Pure + 
73 
options [document_variants = "intro"] 

74 
theories 

75 
files 

48971  76 
"../prepare_document" 
48969  77 
"../pdfsetup.sty" 
78 
"../iman.sty" 

79 
"../extra.sty" 

80 
"../ttbox.sty" 

81 
"../manual.bib" 

82 
"document/build" 

83 
"document/root.tex" 

84 

56420
b266e7a86485
closer correspondence of document and session names, while maintaining document names for external reference
haftmann
parents:
55385
diff
changeset

85 
session Implementation (doc) in "Implementation" = "HOLProofs" + 
48938
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
48937
diff
changeset

86 
options [document_variants = "implementation"] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

87 
theories 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

88 
Eq 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

89 
Integration 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

90 
Isar 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

91 
Local_Theory 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

92 
ML 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

93 
Prelim 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

94 
Proof 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

95 
Syntax 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

96 
Tactic 
52499  97 
theories [parallel_proofs = 0] 
52410  98 
Logic 
48938
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
48937
diff
changeset

99 
files 
48971  100 
"../prepare_document" 
48956  101 
"../pdfsetup.sty" 
48938
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
48937
diff
changeset

102 
"../iman.sty" 
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
48937
diff
changeset

103 
"../extra.sty" 
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
48937
diff
changeset

104 
"../isar.sty" 
49318
612a04e7c853
some attempts to synchronize ROOT/files and document/build;
wenzelm
parents:
48985
diff
changeset

105 
"../ttbox.sty" 
48938
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
48937
diff
changeset

106 
"../underscore.sty" 
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
48937
diff
changeset

107 
"../manual.bib" 
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
48937
diff
changeset

108 
"document/build" 
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
48937
diff
changeset

109 
"document/root.tex" 
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
48937
diff
changeset

110 
"document/style.sty" 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

111 

56420
b266e7a86485
closer correspondence of document and session names, while maintaining document names for external reference
haftmann
parents:
55385
diff
changeset

112 
session "IsarRef" (doc) in "IsarRef" = HOL + 
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset

113 
options [document_variants = "isarref", quick_and_dirty, thy_output_source] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

114 
theories 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

115 
Preface 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

116 
Synopsis 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

117 
Framework 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

118 
First_Order_Logic 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

119 
Outer_Syntax 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

120 
Document_Preparation 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

121 
Spec 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

122 
Proof 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

123 
Inner_Syntax 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

124 
Misc 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

125 
Generic 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

126 
HOL_Specific 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

127 
Quick_Reference 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

128 
Symbols 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

129 
ML_Tactic 
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset

130 
files 
48971  131 
"../prepare_document" 
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset

132 
"../pdfsetup.sty" 
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset

133 
"../iman.sty" 
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset

134 
"../extra.sty" 
49318
612a04e7c853
some attempts to synchronize ROOT/files and document/build;
wenzelm
parents:
48985
diff
changeset

135 
"../isar.sty" 
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset

136 
"../ttbox.sty" 
49318
612a04e7c853
some attempts to synchronize ROOT/files and document/build;
wenzelm
parents:
48985
diff
changeset

137 
"../underscore.sty" 
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset

138 
"../manual.bib" 
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset

139 
"document/build" 
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset

140 
"document/isarvm.pdf" 
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset

141 
"document/isarvm.svg" 
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset

142 
"document/root.tex" 
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset

143 
"document/showsymbols" 
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset

144 
"document/style.sty" 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

145 

54354  146 
session JEdit (doc) in "JEdit" = HOL + 
53769  147 
options [document_variants = "jedit", thy_output_source] 
148 
theories 

149 
JEdit 

150 
files 

56420
b266e7a86485
closer correspondence of document and session names, while maintaining document names for external reference
haftmann
parents:
55385
diff
changeset

151 
"../IsarRef/document/style.sty" 
54331  152 
"../extra.sty" 
153 
"../iman.sty" 

154 
"../isar.sty" 

155 
"../manual.bib" 

53769  156 
"../pdfsetup.sty" 
54331  157 
"../prepare_document" 
53769  158 
"../ttbox.sty" 
159 
"../underscore.sty" 

160 
"document/build" 

54331  161 
"document/isabellejedit.png" 
162 
"document/popup1.png" 

163 
"document/popup2.png" 

53769  164 
"document/root.tex" 
165 

56420
b266e7a86485
closer correspondence of document and session names, while maintaining document names for external reference
haftmann
parents:
55385
diff
changeset

166 
session Sugar (doc) in "Sugar" = HOL + 
48949
a773af3e37d6
more standard document preparation within session context;
wenzelm
parents:
48948
diff
changeset

167 
options [document_variants = "sugar"] 
a773af3e37d6
more standard document preparation within session context;
wenzelm
parents:
48948
diff
changeset

168 
theories [document = ""] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

169 
"~~/src/HOL/Library/LaTeXsugar" 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

170 
"~~/src/HOL/Library/OptionalSugar" 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

171 
theories Sugar 
48949
a773af3e37d6
more standard document preparation within session context;
wenzelm
parents:
48948
diff
changeset

172 
files 
48971  173 
"../prepare_document" 
48956  174 
"../pdfsetup.sty" 
48949
a773af3e37d6
more standard document preparation within session context;
wenzelm
parents:
48948
diff
changeset

175 
"document/build" 
a773af3e37d6
more standard document preparation within session context;
wenzelm
parents:
48948
diff
changeset

176 
"document/mathpartir.sty" 
a773af3e37d6
more standard document preparation within session context;
wenzelm
parents:
48948
diff
changeset

177 
"document/root.bib" 
a773af3e37d6
more standard document preparation within session context;
wenzelm
parents:
48948
diff
changeset

178 
"document/root.tex" 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

179 

48943
54da920baf38
more standard document preparation within session context;
wenzelm
parents:
48942
diff
changeset

180 
session Locales (doc) in "Locales" = 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:
51397
diff
changeset

181 
options [document_variants = "locales", pretty_margin = 65, skip_proofs = false] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

182 
theories 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

183 
Examples1 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

184 
Examples2 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

185 
Examples3 
48943
54da920baf38
more standard document preparation within session context;
wenzelm
parents:
48942
diff
changeset

186 
files 
48971  187 
"../prepare_document" 
48956  188 
"../pdfsetup.sty" 
48943
54da920baf38
more standard document preparation within session context;
wenzelm
parents:
48942
diff
changeset

189 
"document/build" 
54da920baf38
more standard document preparation within session context;
wenzelm
parents:
48942
diff
changeset

190 
"document/root.tex" 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

191 

48942
75d8778f94d3
more standard document preparation within session context;
wenzelm
parents:
48941
diff
changeset

192 
session Logics (doc) in "Logics" = Pure + 
75d8778f94d3
more standard document preparation within session context;
wenzelm
parents:
48941
diff
changeset

193 
options [document_variants = "logics"] 
75d8778f94d3
more standard document preparation within session context;
wenzelm
parents:
48941
diff
changeset

194 
theories 
75d8778f94d3
more standard document preparation within session context;
wenzelm
parents:
48941
diff
changeset

195 
files 
48971  196 
"../prepare_document" 
48956  197 
"../pdfsetup.sty" 
48942
75d8778f94d3
more standard document preparation within session context;
wenzelm
parents:
48941
diff
changeset

198 
"../iman.sty" 
75d8778f94d3
more standard document preparation within session context;
wenzelm
parents:
48941
diff
changeset

199 
"../extra.sty" 
75d8778f94d3
more standard document preparation within session context;
wenzelm
parents:
48941
diff
changeset

200 
"../ttbox.sty" 
75d8778f94d3
more standard document preparation within session context;
wenzelm
parents:
48941
diff
changeset

201 
"../manual.bib" 
52552
0260bdba4dd7
reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;
wenzelm
parents:
52499
diff
changeset

202 
"document/CTT.tex" 
0260bdba4dd7
reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;
wenzelm
parents:
52499
diff
changeset

203 
"document/HOL.tex" 
0260bdba4dd7
reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;
wenzelm
parents:
52499
diff
changeset

204 
"document/LK.tex" 
0260bdba4dd7
reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;
wenzelm
parents:
52499
diff
changeset

205 
"document/Sequents.tex" 
48942
75d8778f94d3
more standard document preparation within session context;
wenzelm
parents:
48941
diff
changeset

206 
"document/build" 
52552
0260bdba4dd7
reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;
wenzelm
parents:
52499
diff
changeset

207 
"document/preface.tex" 
48942
75d8778f94d3
more standard document preparation within session context;
wenzelm
parents:
48941
diff
changeset

208 
"document/root.tex" 
52552
0260bdba4dd7
reduced number of old manuals: chapter HOL is back again to the Logics manual by Larry;
wenzelm
parents:
52499
diff
changeset

209 
"document/syntax.tex" 
48945
b5758f5a469c
more standard document preparation within session context;
wenzelm
parents:
48944
diff
changeset

210 

56420
b266e7a86485
closer correspondence of document and session names, while maintaining document names for external reference
haftmann
parents:
55385
diff
changeset

211 
session "LogicsZF" (doc) in "LogicsZF" = ZF + 
48956  212 
options [document_variants = "logicsZF", print_mode = "brackets", 
213 
thy_output_source] 

48946
a9b8344f5196
more standard document preparation within session context;
wenzelm
parents:
48945
diff
changeset

214 
theories 
a9b8344f5196
more standard document preparation within session context;
wenzelm
parents:
48945
diff
changeset

215 
IFOL_examples 
a9b8344f5196
more standard document preparation within session context;
wenzelm
parents:
48945
diff
changeset

216 
FOL_examples 
a9b8344f5196
more standard document preparation within session context;
wenzelm
parents:
48945
diff
changeset

217 
ZF_examples 
a9b8344f5196
more standard document preparation within session context;
wenzelm
parents:
48945
diff
changeset

218 
If 
48956  219 
ZF_Isar 
48946
a9b8344f5196
more standard document preparation within session context;
wenzelm
parents:
48945
diff
changeset

220 
files 
48971  221 
"../prepare_document" 
48956  222 
"../pdfsetup.sty" 
223 
"../isar.sty" 

48946
a9b8344f5196
more standard document preparation within session context;
wenzelm
parents:
48945
diff
changeset

224 
"../ttbox.sty" 
a9b8344f5196
more standard document preparation within session context;
wenzelm
parents:
48945
diff
changeset

225 
"../manual.bib" 
a9b8344f5196
more standard document preparation within session context;
wenzelm
parents:
48945
diff
changeset

226 
"../Logics/document/syntax.tex" 
a9b8344f5196
more standard document preparation within session context;
wenzelm
parents:
48945
diff
changeset

227 
"document/build" 
a9b8344f5196
more standard document preparation within session context;
wenzelm
parents:
48945
diff
changeset

228 
"document/root.tex" 
a9b8344f5196
more standard document preparation within session context;
wenzelm
parents:
48945
diff
changeset

229 

48944
ac15a85e9282
more standard document preparation within session context;
wenzelm
parents:
48943
diff
changeset

230 
session Main (doc) in "Main" = HOL + 
ac15a85e9282
more standard document preparation within session context;
wenzelm
parents:
48943
diff
changeset

231 
options [document_variants = "main"] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

232 
theories Main_Doc 
48944
ac15a85e9282
more standard document preparation within session context;
wenzelm
parents:
48943
diff
changeset

233 
files 
48971  234 
"../prepare_document" 
48956  235 
"../pdfsetup.sty" 
48944
ac15a85e9282
more standard document preparation within session context;
wenzelm
parents:
48943
diff
changeset

236 
"document/build" 
ac15a85e9282
more standard document preparation within session context;
wenzelm
parents:
48943
diff
changeset

237 
"document/root.tex" 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

238 

48963
f11d88bfa934
more standard document preparation within session context;
wenzelm
parents:
48962
diff
changeset

239 
session Nitpick (doc) in "Nitpick" = Pure + 
f11d88bfa934
more standard document preparation within session context;
wenzelm
parents:
48962
diff
changeset

240 
options [document_variants = "nitpick"] 
f11d88bfa934
more standard document preparation within session context;
wenzelm
parents:
48962
diff
changeset

241 
theories 
f11d88bfa934
more standard document preparation within session context;
wenzelm
parents:
48962
diff
changeset

242 
files 
48971  243 
"../prepare_document" 
48963
f11d88bfa934
more standard document preparation within session context;
wenzelm
parents:
48962
diff
changeset

244 
"../pdfsetup.sty" 
f11d88bfa934
more standard document preparation within session context;
wenzelm
parents:
48962
diff
changeset

245 
"../iman.sty" 
f11d88bfa934
more standard document preparation within session context;
wenzelm
parents:
48962
diff
changeset

246 
"../manual.bib" 
f11d88bfa934
more standard document preparation within session context;
wenzelm
parents:
48962
diff
changeset

247 
"document/build" 
f11d88bfa934
more standard document preparation within session context;
wenzelm
parents:
48962
diff
changeset

248 
"document/root.tex" 
f11d88bfa934
more standard document preparation within session context;
wenzelm
parents:
48962
diff
changeset

249 

56420
b266e7a86485
closer correspondence of document and session names, while maintaining document names for external reference
haftmann
parents:
55385
diff
changeset

250 
session "ProgProve" (doc) in "ProgProve" = HOL + 
48947
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
48946
diff
changeset

251 
options [document_variants = "progprove", show_question_marks = false] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

252 
theories 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

253 
Basics 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

254 
Bool_nat_list 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

255 
MyList 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

256 
Types_and_funs 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

257 
Logic 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

258 
Isar 
48947
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
48946
diff
changeset

259 
files 
48971  260 
"../prepare_document" 
48956  261 
"../pdfsetup.sty" 
48947
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
48946
diff
changeset

262 
"document/bang.pdf" 
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
48946
diff
changeset

263 
"document/build" 
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
48946
diff
changeset

264 
"document/introisabelle.tex" 
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
48946
diff
changeset

265 
"document/mathpartir.sty" 
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
48946
diff
changeset

266 
"document/prelude.tex" 
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
48946
diff
changeset

267 
"document/root.bib" 
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
48946
diff
changeset

268 
"document/root.tex" 
7eee8b2d2099
more standard document preparation within session context;
wenzelm
parents:
48946
diff
changeset

269 
"document/svmono.cls" 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

270 

48962
a1acc1cb0271
more standard document preparation within session context;
wenzelm
parents:
48961
diff
changeset

271 
session Sledgehammer (doc) in "Sledgehammer" = Pure + 
a1acc1cb0271
more standard document preparation within session context;
wenzelm
parents:
48961
diff
changeset

272 
options [document_variants = "sledgehammer"] 
a1acc1cb0271
more standard document preparation within session context;
wenzelm
parents:
48961
diff
changeset

273 
theories 
a1acc1cb0271
more standard document preparation within session context;
wenzelm
parents:
48961
diff
changeset

274 
files 
48971  275 
"../prepare_document" 
48962
a1acc1cb0271
more standard document preparation within session context;
wenzelm
parents:
48961
diff
changeset

276 
"../pdfsetup.sty" 
a1acc1cb0271
more standard document preparation within session context;
wenzelm
parents:
48961
diff
changeset

277 
"../iman.sty" 
a1acc1cb0271
more standard document preparation within session context;
wenzelm
parents:
48961
diff
changeset

278 
"../manual.bib" 
a1acc1cb0271
more standard document preparation within session context;
wenzelm
parents:
48961
diff
changeset

279 
"document/build" 
a1acc1cb0271
more standard document preparation within session context;
wenzelm
parents:
48961
diff
changeset

280 
"document/root.tex" 
a1acc1cb0271
more standard document preparation within session context;
wenzelm
parents:
48961
diff
changeset

281 

48937
e7418f8d49fe
more standard document preparation within session context;
wenzelm
parents:
48738
diff
changeset

282 
session System (doc) in "System" = Pure + 
e7418f8d49fe
more standard document preparation within session context;
wenzelm
parents:
48738
diff
changeset

283 
options [document_variants = "system", thy_output_source] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

284 
theories 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

285 
Basics 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

286 
Interfaces 
48578  287 
Sessions 
288 
Presentation 

48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

289 
Scala 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

290 
Misc 
48937
e7418f8d49fe
more standard document preparation within session context;
wenzelm
parents:
48738
diff
changeset

291 
files 
48971  292 
"../prepare_document" 
56420
b266e7a86485
closer correspondence of document and session names, while maintaining document names for external reference
haftmann
parents:
55385
diff
changeset

293 
"../IsarRef/document/style.sty" 
48956  294 
"../pdfsetup.sty" 
48937
e7418f8d49fe
more standard document preparation within session context;
wenzelm
parents:
48738
diff
changeset

295 
"../iman.sty" 
e7418f8d49fe
more standard document preparation within session context;
wenzelm
parents:
48738
diff
changeset

296 
"../extra.sty" 
49318
612a04e7c853
some attempts to synchronize ROOT/files and document/build;
wenzelm
parents:
48985
diff
changeset

297 
"../isar.sty" 
48937
e7418f8d49fe
more standard document preparation within session context;
wenzelm
parents:
48738
diff
changeset

298 
"../ttbox.sty" 
e7418f8d49fe
more standard document preparation within session context;
wenzelm
parents:
48738
diff
changeset

299 
"../underscore.sty" 
e7418f8d49fe
more standard document preparation within session context;
wenzelm
parents:
48738
diff
changeset

300 
"../manual.bib" 
e7418f8d49fe
more standard document preparation within session context;
wenzelm
parents:
48738
diff
changeset

301 
"document/browser_screenshot.png" 
e7418f8d49fe
more standard document preparation within session context;
wenzelm
parents:
48738
diff
changeset

302 
"document/build" 
e7418f8d49fe
more standard document preparation within session context;
wenzelm
parents:
48738
diff
changeset

303 
"document/root.tex" 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

304 

48985  305 
session Tutorial (doc) in "Tutorial" = 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:
51397
diff
changeset

306 
options [document_variants = "tutorial", print_mode = "brackets", skip_proofs = false] 
53376  307 
theories [threads = 1] 
308 
"ToyList/ToyList_Test" 

48526  309 
theories [thy_output_indent = 5] 
310 
"ToyList/ToyList" 

311 
"Ifexpr/Ifexpr" 

312 
"CodeGen/CodeGen" 

313 
"Trie/Trie" 

314 
"Datatype/ABexpr" 

315 
"Datatype/unfoldnested" 

316 
"Datatype/Nested" 

317 
"Datatype/Fundata" 

318 
"Fun/fun0" 

319 
"Advanced/simp2" 

320 
"CTL/PDL" 

321 
"CTL/CTL" 

322 
"CTL/CTLind" 

323 
"Inductive/Even" 

324 
"Inductive/Mutual" 

325 
"Inductive/Star" 

326 
"Inductive/AB" 

327 
"Inductive/Advanced" 

328 
"Misc/Tree" 

329 
"Misc/Tree2" 

330 
"Misc/Plus" 

331 
"Misc/case_exprs" 

332 
"Misc/fakenat" 

333 
"Misc/natsum" 

334 
"Misc/pairs2" 

335 
"Misc/Option2" 

336 
"Misc/types" 

337 
"Misc/prime_def" 

338 
"Misc/simp" 

339 
"Misc/Itrev" 

340 
"Misc/AdvancedInd" 

341 
"Misc/appendix" 

342 
theories 

343 
"Protocol/NS_Public" 

344 
"Documents/Documents" 

48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on caseinsensible filesystem;
wenzelm
parents:
48963
diff
changeset

345 
theories [document = ""] 
48526  346 
"Types/Setup" 
48611
b34ff75c23a7
multithreaded HOLTutorial with explicit indication of local options;
wenzelm
parents:
48587
diff
changeset

347 
theories [pretty_margin = 64, thy_output_indent = 0] 
48526  348 
"Types/Numbers" 
349 
"Types/Pairs" 

350 
"Types/Records" 

351 
"Types/Typedefs" 

352 
"Types/Overloading" 

353 
"Types/Axioms" 

354 
"Rules/Basic" 

355 
"Rules/Blast" 

356 
"Rules/Force" 

48611
b34ff75c23a7
multithreaded HOLTutorial with explicit indication of local options;
wenzelm
parents:
48587
diff
changeset

357 
theories [pretty_margin = 64, thy_output_indent = 5] 
55159
608c157d743d
Replacing the theory Library/Binomial by Number_Theory/Binomial
paulson <lp15@cam.ac.uk>
parents:
55073
diff
changeset

358 
"Rules/TPrimes" 
48526  359 
"Rules/Forward" 
360 
"Rules/Tacticals" 

361 
"Rules/find2" 

362 
"Sets/Examples" 

363 
"Sets/Functions" 

364 
"Sets/Relations" 

365 
"Sets/Recur" 

48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on caseinsensible filesystem;
wenzelm
parents:
48963
diff
changeset

366 
files 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on caseinsensible filesystem;
wenzelm
parents:
48963
diff
changeset

367 
"ToyList/ToyList1" 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on caseinsensible filesystem;
wenzelm
parents:
48963
diff
changeset

368 
"ToyList/ToyList2" 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on caseinsensible filesystem;
wenzelm
parents:
48963
diff
changeset

369 
"../pdfsetup.sty" 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on caseinsensible filesystem;
wenzelm
parents:
48963
diff
changeset

370 
"../ttbox.sty" 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on caseinsensible filesystem;
wenzelm
parents:
48963
diff
changeset

371 
"../manual.bib" 
48968
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

372 
"document/advanced0.tex" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

373 
"document/appendix0.tex" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

374 
"document/basics.tex" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

375 
"document/build" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

376 
"document/cl2emonomodified.sty" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

377 
"document/ctl0.tex" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

378 
"document/documents0.tex" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

379 
"document/fp.tex" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

380 
"document/inductive0.tex" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

381 
"document/isaindex" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

382 
"document/Isalogics.pdf" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

383 
"document/numerics.tex" 
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on caseinsensible filesystem;
wenzelm
parents:
48963
diff
changeset

384 
"document/pghead.pdf" 
48968
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

385 
"document/preface.tex" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

386 
"document/protocol.tex" 
48966
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on caseinsensible filesystem;
wenzelm
parents:
48963
diff
changeset

387 
"document/root.tex" 
48968
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

388 
"document/rules.tex" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

389 
"document/sets.tex" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

390 
"document/tutorial.sty" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

391 
"document/typedef.pdf" 
5e83c70266cf
prefer (old) isaindex as provided here, to get exactly the same index layout as in Isabelle2012;
wenzelm
parents:
48966
diff
changeset

392 
"document/types0.tex" 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

393 