author  wenzelm 
Sat, 28 Jul 2012 20:20:35 +0200  
changeset 48587  f9732774ffc7 
parent 48578  21361b6189a6 
child 48611  b34ff75c23a7 
permissions  rwrr 
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 docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

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

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

6 

48509  7 
session Codegen! (doc) in "Codegen/Thy" = "HOLLibrary" + 
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 docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

10 
print_mode = "no_brackets,iff"] 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

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

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

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

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

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

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

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

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

19 
Further 
fd03877ad5bc
session specifications for docsrc, 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 docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

24 
theories Functions 
fd03877ad5bc
session specifications for docsrc, 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 docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

39 
Tactic 
fd03877ad5bc
session specifications for docsrc, 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 docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

44 
quick_and_dirty] 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

60 
ML_Tactic 
fd03877ad5bc
session specifications for docsrc, 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 docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

65 
quick_and_dirty] 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

66 
theories HOLCF_Specific 
fd03877ad5bc
session specifications for docsrc, 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 docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

71 
quick_and_dirty] 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

72 
theories ZF_Specific 
fd03877ad5bc
session specifications for docsrc, 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, 
48587  76 
document_dump = document, document_dump_mode = "tex"] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

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

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

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

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

81 

48509  82 
session Locales! (doc) in "Locales/Locales" = HOL + 
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48509
diff
changeset

83 
options [browser_info = false, document = false, 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48509
diff
changeset

84 
document_dump = document, document_dump_mode = "tex"] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

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

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

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

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

89 

48509  90 
session Main! (doc) in "Main/Docs" = HOL + 
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48509
diff
changeset

91 
options [browser_info = false, document = false, 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48509
diff
changeset

92 
document_dump = document, document_dump_mode = "tex"] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

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

94 

48509  95 
session ProgProve! (doc) in "ProgProve/Thys" = HOL + 
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48509
diff
changeset

96 
options [browser_info = false, document = false, 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48509
diff
changeset

97 
document_dump = document, document_dump_mode = "tex", 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

98 
show_question_marks = false] 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

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

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

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

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

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

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

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

106 

48509  107 
session System! (doc) in "System/Thy" = Pure + 
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48509
diff
changeset

108 
options [browser_info = false, document = false, 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48509
diff
changeset

109 
document_dump = document, document_dump_mode = "tex"] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

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

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

112 
Interfaces 
48578  113 
Sessions 
114 
Presentation 

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

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

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

117 

48526  118 
session Tutorial (doc) in "TutorialI" = HOL + 
119 
options [browser_info = false, document = false, 

120 
document_dump = document, document_dump_mode = "tex", 

121 
print_mode = "brackets", threads = 1 (* FIXME *)] 

122 
theories [thy_output_indent = 5] 

123 
"ToyList/ToyList" 

124 
"Ifexpr/Ifexpr" 

125 
"CodeGen/CodeGen" 

126 
"Trie/Trie" 

127 
"Datatype/ABexpr" 

128 
"Datatype/unfoldnested" 

129 
"Datatype/Nested" 

130 
"Datatype/Fundata" 

131 
"Fun/fun0" 

132 
"Advanced/simp2" 

133 
"CTL/PDL" 

134 
"CTL/CTL" 

135 
"CTL/CTLind" 

136 
"Inductive/Even" 

137 
"Inductive/Mutual" 

138 
"Inductive/Star" 

139 
"Inductive/AB" 

140 
"Inductive/Advanced" 

141 
"Misc/Tree" 

142 
"Misc/Tree2" 

143 
"Misc/Plus" 

144 
"Misc/case_exprs" 

145 
"Misc/fakenat" 

146 
"Misc/natsum" 

147 
"Misc/pairs2" 

148 
"Misc/Option2" 

149 
"Misc/types" 

150 
"Misc/prime_def" 

151 
"Misc/simp" 

152 
"Misc/Itrev" 

153 
"Misc/AdvancedInd" 

154 
"Misc/appendix" 

155 
theories 

156 
"Protocol/NS_Public" 

157 
"Documents/Documents" 

158 
theories [document_dump = ""] 

159 
"Types/Setup" 

160 
theories 

161 
"Types/Numbers" 

162 
"Types/Pairs" 

163 
"Types/Records" 

164 
"Types/Typedefs" 

165 
"Types/Overloading" 

166 
"Types/Axioms" 

167 
"Rules/Basic" 

168 
"Rules/Blast" 

169 
"Rules/Force" 

170 
"Rules/Forward" 

171 
"Rules/Tacticals" 

172 
"Rules/find2" 

173 
"Sets/Examples" 

174 
"Sets/Functions" 

175 
"Sets/Relations" 

176 
"Sets/Recur" 

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

177 

48509  178 
session examples (doc) in "ZF" = ZF + 
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48509
diff
changeset

179 
options [browser_info = false, document = false, 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48509
diff
changeset

180 
document_dump = document, document_dump_mode = "tex", 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

181 
print_mode = "brackets"] 
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 
IFOL_examples 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

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

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

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

187 