equal
deleted
inserted
replaced
107 ML_file "Tools/find_theorems.ML" |
107 ML_file "Tools/find_theorems.ML" |
108 ML_file "Tools/find_consts.ML" |
108 ML_file "Tools/find_consts.ML" |
109 ML_file "Tools/simplifier_trace.ML" |
109 ML_file "Tools/simplifier_trace.ML" |
110 ML_file "Tools/debugger.ML" |
110 ML_file "Tools/debugger.ML" |
111 ML_file "Tools/named_theorems.ML" |
111 ML_file "Tools/named_theorems.ML" |
|
112 ML_file "Tools/jedit.ML" |
112 |
113 |
113 |
114 |
114 section \<open>Basic attributes\<close> |
115 section \<open>Basic attributes\<close> |
115 |
116 |
116 attribute_setup tagged = |
117 attribute_setup tagged = |
296 from conj show "PROP B" by (rule conjunctionD2) |
297 from conj show "PROP B" by (rule conjunctionD2) |
297 qed |
298 qed |
298 qed |
299 qed |
299 |
300 |
300 end |
301 end |
301 |
|