changeset 60754 | 02924903a6fd |
parent 58889 | 5b7a9633cfa8 |
child 61069 | aefe89038dd2 |
--- a/src/HOL/IMPP/Com.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/IMPP/Com.thy Sat Jul 18 20:54:56 2015 +0200 @@ -83,7 +83,10 @@ "WT_bodies = (!(pn,b):set bodies. WT b)" -ML {* val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl] *} +ML {* + fun make_imp_tac ctxt = + EVERY' [resolve_tac ctxt [mp], fn i => assume_tac ctxt (i + 1), eresolve_tac ctxt [thin_rl]] +*} lemma finite_dom_body: "finite (dom body)" apply (unfold body_def)