author  wenzelm 
Mon, 27 Aug 2012 21:19:16 +0200  
changeset 48943  54da920baf38 
parent 48942  75d8778f94d3 
child 48944  ac15a85e9282 
permissions  rwrr 
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48612
diff
changeset

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 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48612
diff
changeset

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 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48612
diff
changeset

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 

48938
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
48937
diff
changeset

26 
session IsarImplementation (doc) in "IsarImplementation" = HOL + 
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
48937
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

38 
Tactic 
48938
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
48937
diff
changeset

39 
files 
d468d72a458f
more standard document preparation within session context;
wenzelm
parents:
48937
diff
changeset

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

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

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

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

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

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

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

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

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

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

50 

48941
fbf60999dc31
more standard document preparation within session context;
wenzelm
parents:
48939
diff
changeset

51 
session Intro (doc) in "Intro" = Pure + 
fbf60999dc31
more standard document preparation within session context;
wenzelm
parents:
48939
diff
changeset

52 
options [document_variants = "intro"] 
fbf60999dc31
more standard document preparation within session context;
wenzelm
parents:
48939
diff
changeset

53 
theories 
fbf60999dc31
more standard document preparation within session context;
wenzelm
parents:
48939
diff
changeset

54 
files 
fbf60999dc31
more standard document preparation within session context;
wenzelm
parents:
48939
diff
changeset

55 
"../iman.sty" 
fbf60999dc31
more standard document preparation within session context;
wenzelm
parents:
48939
diff
changeset

56 
"../extra.sty" 
fbf60999dc31
more standard document preparation within session context;
wenzelm
parents:
48939
diff
changeset

57 
"../ttbox.sty" 
fbf60999dc31
more standard document preparation within session context;
wenzelm
parents:
48939
diff
changeset

58 
"../proof.sty" 
fbf60999dc31
more standard document preparation within session context;
wenzelm
parents:
48939
diff
changeset

59 
"../manual.bib" 
fbf60999dc31
more standard document preparation within session context;
wenzelm
parents:
48939
diff
changeset

60 
"document/build" 
fbf60999dc31
more standard document preparation within session context;
wenzelm
parents:
48939
diff
changeset

61 
"document/root.tex" 
fbf60999dc31
more standard document preparation within session context;
wenzelm
parents:
48939
diff
changeset

62 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48612
diff
changeset

63 
session "HOLIsarRef" (doc) in "IsarRef/Thy" = HOL + 
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48509
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

83 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48612
diff
changeset

84 
session "HOLCFIsarRef" (doc) in "IsarRef/Thy" = HOLCF + 
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48509
diff
changeset

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

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

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

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

89 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48612
diff
changeset

90 
session "ZFIsarRef" (doc) in "IsarRef/Thy" = ZF + 
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 
quick_and_dirty] 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

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

95 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48612
diff
changeset

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

97 
options [browser_info = false, document = false, 
48587  98 
document_dump = document, document_dump_mode = "tex"] 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

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

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

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

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

103 

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

104 
session Locales (doc) in "Locales" = HOL + 
54da920baf38
more standard document preparation within session context;
wenzelm
parents:
48942
diff
changeset

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

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

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

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

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

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

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

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

113 

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

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

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

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

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

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

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

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

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

122 
"../manual.bib" 
75d8778f94d3
more standard document preparation within session context;
wenzelm
parents:
48941
diff
changeset

123 
"document/build" 
75d8778f94d3
more standard document preparation within session context;
wenzelm
parents:
48941
diff
changeset

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

125 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48612
diff
changeset

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

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

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

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

130 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48612
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

142 

48939
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

143 
session Ref (doc) in "Ref" = Pure + 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

144 
options [document_variants = "ref"] 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

145 
theories 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

146 
files 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

147 
"../iman.sty" 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

148 
"../extra.sty" 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

149 
"../ttbox.sty" 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

150 
"../proof.sty" 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

151 
"../manual.bib" 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

152 
"document/build" 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

153 
"document/classical.tex" 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

154 
"document/root.tex" 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

155 
"document/simplifier.tex" 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

156 
"document/substitution.tex" 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

157 
"document/syntax.tex" 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

158 
"document/tactic.tex" 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

159 
"document/thm.tex" 
83bd9eb1c70c
more standard document preparation within session context;
wenzelm
parents:
48938
diff
changeset

160 

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

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

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

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

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

165 
Interfaces 
48578  166 
Sessions 
167 
Presentation 

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

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

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

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

171 
"../IsarRef/style.sty" 
e7418f8d49fe
more standard document preparation within session context;
wenzelm
parents:
48738
diff
changeset

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

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

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

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

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

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

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

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

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

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

182 

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

185 
document_dump = document, document_dump_mode = "tex", 

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

186 
print_mode = "brackets"] 
48526  187 
theories [thy_output_indent = 5] 
188 
"ToyList/ToyList" 

189 
"Ifexpr/Ifexpr" 

190 
"CodeGen/CodeGen" 

191 
"Trie/Trie" 

192 
"Datatype/ABexpr" 

193 
"Datatype/unfoldnested" 

194 
"Datatype/Nested" 

195 
"Datatype/Fundata" 

196 
"Fun/fun0" 

197 
"Advanced/simp2" 

198 
"CTL/PDL" 

199 
"CTL/CTL" 

200 
"CTL/CTLind" 

201 
"Inductive/Even" 

202 
"Inductive/Mutual" 

203 
"Inductive/Star" 

204 
"Inductive/AB" 

205 
"Inductive/Advanced" 

206 
"Misc/Tree" 

207 
"Misc/Tree2" 

208 
"Misc/Plus" 

209 
"Misc/case_exprs" 

210 
"Misc/fakenat" 

211 
"Misc/natsum" 

212 
"Misc/pairs2" 

213 
"Misc/Option2" 

214 
"Misc/types" 

215 
"Misc/prime_def" 

216 
"Misc/simp" 

217 
"Misc/Itrev" 

218 
"Misc/AdvancedInd" 

219 
"Misc/appendix" 

220 
theories 

221 
"Protocol/NS_Public" 

222 
"Documents/Documents" 

223 
theories [document_dump = ""] 

224 
"Types/Setup" 

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

225 
theories [pretty_margin = 64, thy_output_indent = 0] 
48526  226 
"Types/Numbers" 
227 
"Types/Pairs" 

228 
"Types/Records" 

229 
"Types/Typedefs" 

230 
"Types/Overloading" 

231 
"Types/Axioms" 

232 
"Rules/Basic" 

233 
"Rules/Blast" 

234 
"Rules/Force" 

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

235 
theories [pretty_margin = 64, thy_output_indent = 5] 
b34ff75c23a7
multithreaded HOLTutorial with explicit indication of local options;
wenzelm
parents:
48587
diff
changeset

236 
"Rules/Primes" 
48526  237 
"Rules/Forward" 
238 
"Rules/Tacticals" 

239 
"Rules/find2" 

240 
"Sets/Examples" 

241 
"Sets/Functions" 

242 
"Sets/Relations" 

243 
"Sets/Recur" 

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

244 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48612
diff
changeset

245 
session "HOLToyList2" (doc) in "TutorialI/ToyList2" = HOL + 
48612
795d38a6dab3
regenerate ToyList2/ToyList.thy during raw make *after* session build, to ensure that it is updated sporadically (NB: isabelle build does not support generated sources);
wenzelm
parents:
48611
diff
changeset

246 
options [browser_info = false, document = false, print_mode = "brackets"] 
795d38a6dab3
regenerate ToyList2/ToyList.thy during raw make *after* session build, to ensure that it is updated sporadically (NB: isabelle build does not support generated sources);
wenzelm
parents:
48611
diff
changeset

247 
theories ToyList 
795d38a6dab3
regenerate ToyList2/ToyList.thy during raw make *after* session build, to ensure that it is updated sporadically (NB: isabelle build does not support generated sources);
wenzelm
parents:
48611
diff
changeset

248 

48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48612
diff
changeset

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

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

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

252 
print_mode = "brackets"] 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

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

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

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

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

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

258 