91 and "extract_type" "extract" :: thy_decl |
91 and "extract_type" "extract" :: thy_decl |
92 and "find_theorems" "find_consts" :: diag |
92 and "find_theorems" "find_consts" :: diag |
93 and "named_theorems" :: thy_decl |
93 and "named_theorems" :: thy_decl |
94 begin |
94 begin |
95 |
95 |
96 ML_file "ML/ml_antiquotations.ML" |
|
97 ML_file "ML/ml_thms.ML" |
|
98 ML_file "Tools/print_operation.ML" |
|
99 ML_file "Isar/isar_syn.ML" |
96 ML_file "Isar/isar_syn.ML" |
100 ML_file "Isar/calculation.ML" |
|
101 ML_file "Tools/bibtex.ML" |
|
102 ML_file "Tools/rail.ML" |
|
103 ML_file "Tools/rule_insts.ML" |
|
104 ML_file "Tools/thm_deps.ML" |
|
105 ML_file "Tools/thy_deps.ML" |
|
106 ML_file "Tools/class_deps.ML" |
|
107 ML_file "Tools/find_theorems.ML" |
|
108 ML_file "Tools/find_consts.ML" |
|
109 ML_file "Tools/simplifier_trace.ML" |
|
110 ML_file_no_debug "Tools/debugger.ML" |
|
111 ML_file "Tools/named_theorems.ML" |
|
112 ML_file "Tools/jedit.ML" |
|
113 |
97 |
114 |
98 |
115 section \<open>Basic attributes\<close> |
99 section \<open>Basic attributes\<close> |
116 |
100 |
117 attribute_setup tagged = |
101 attribute_setup tagged = |