equal
deleted
inserted
replaced
194 fun merge _ = Thm.merge_thms; |
194 fun merge _ = Thm.merge_thms; |
195 ); |
195 ); |
196 |
196 |
197 fun print_rules ctxt = |
197 fun print_rules ctxt = |
198 Pretty.writeln (Pretty.big_list "definitional transformations:" |
198 Pretty.writeln (Pretty.big_list "definitional transformations:" |
199 (map (ProofContext.pretty_thm ctxt) (Rules.get (Context.Proof ctxt)))); |
199 (map (Display.pretty_thm ctxt) (Rules.get (Context.Proof ctxt)))); |
200 |
200 |
201 val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm); |
201 val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm); |
202 val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm); |
202 val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm); |
203 |
203 |
204 |
204 |