equal
deleted
inserted
replaced
254 in CHANGED_GOAL (rtac (th' RS ssubst)) end; |
254 in CHANGED_GOAL (rtac (th' RS ssubst)) end; |
255 |
255 |
256 |
256 |
257 (* proof methods *) |
257 (* proof methods *) |
258 |
258 |
259 val subst_meth = Method.goal_args' Attrib.local_thm stac; |
259 val subst_meth = Method.thm_args (Method.SIMPLE_METHOD' HEADGOAL o stac); |
260 val hyp_subst_meth = Method.goal_args (Scan.succeed ()) (K hyp_subst_tac); |
260 val hyp_subst_meth = Method.no_args (Method.SIMPLE_METHOD' HEADGOAL hyp_subst_tac); |
261 |
261 |
262 |
262 |
263 (* attributes *) |
263 (* attributes *) |
264 |
264 |
265 fun symmetric_rule thm = |
265 fun symmetric_rule thm = |