author  wenzelm 
Thu, 26 Jul 2012 14:29:54 +0200  
changeset 48516  c5d0f19ef7cb 
parent 48509  4854ced3e9d7 
child 48526  4372b7cb858d 
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, 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48509
diff
changeset

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

77 
threads = 1] (* FIXME *) 
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

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

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

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

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

82 

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

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

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

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

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

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

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

90 

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

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

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

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

95 

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

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

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

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

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

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

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

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

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

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

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

107 

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

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

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

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

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

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

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

115 
Presentation 
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 

48509  118 
(* session Tutorial (doc) in "Tutorial" = HOL + FIXME *) 
48502
fd03877ad5bc
session specifications for docsrc, excluding TutorialI for now;
wenzelm
parents:
diff
changeset

119 

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

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

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

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

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

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

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

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

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

129 