src/Provers/hypsubst.ML
changeset 9705 8eecca293907
parent 9628 53a62fd8b2dc
child 9893 93d2fde0306c
equal deleted inserted replaced
9704:c2f2f70bbb60 9705:8eecca293907
   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 =