equal
deleted
inserted
replaced
255 |
255 |
256 |
256 |
257 (* proof methods *) |
257 (* proof methods *) |
258 |
258 |
259 val subst_meth = Method.thm_args (Method.SIMPLE_METHOD' HEADGOAL o stac); |
259 val subst_meth = Method.thm_args (Method.SIMPLE_METHOD' HEADGOAL o stac); |
260 val hyp_subst_meth = Method.no_args (Method.SIMPLE_METHOD' HEADGOAL hyp_subst_tac); |
260 val hyp_subst_meth = |
|
261 Method.no_args (Method.SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o hyp_subst_tac)); |
261 |
262 |
262 |
263 |
263 (* attributes *) |
264 (* attributes *) |
264 |
265 |
265 fun symmetric_rule thm = |
266 fun symmetric_rule thm = |