# HG changeset patch # User nipkow # Date 1050339165 -7200 # Node ID f5c3750292f5501832f90a91e4e8a67cd3e95308 # Parent f9a9ef16466fc04cc969ef41975acc8d34eb0d9b added thm"..." due to new Map.thy diff -r f9a9ef16466f -r f5c3750292f5 src/HOL/IMPP/Com.ML --- a/src/HOL/IMPP/Com.ML Mon Apr 14 18:52:13 2003 +0200 +++ b/src/HOL/IMPP/Com.ML Mon Apr 14 18:52:45 2003 +0200 @@ -1,11 +1,11 @@ val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl]; Goalw [body_def] "finite (dom body)"; -by (rtac finite_dom_map_of 1); +by (rtac (thm"finite_dom_map_of") 1); qed "finite_dom_body"; Goalw [WT_bodies_def, body_def] "[| WT_bodies; body pn = Some b |] ==> WT b"; -by (dtac map_of_SomeD 1); +by (dtac (thm"map_of_SomeD") 1); by (Fast_tac 1); qed "WT_bodiesD"; diff -r f9a9ef16466f -r f5c3750292f5 src/HOL/IMPP/Hoare.ML --- a/src/HOL/IMPP/Hoare.ML Mon Apr 14 18:52:13 2003 +0200 +++ b/src/HOL/IMPP/Hoare.ML Mon Apr 14 18:52:45 2003 +0200 @@ -230,10 +230,10 @@ \ !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}"; by (induct_tac "c" 1); by (ALLGOALS Clarsimp_tac); -by (fast_tac (claset() addIs [domI]) 7); +by (fast_tac (claset() addIs [(thm"domI")]) 7); by (etac MGT_alternD 6); by (rewtac MGT_def); -by (EVERY'[dtac bspec, etac domI] 7); +by (EVERY'[dtac bspec, etac (thm"domI")] 7); by (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac [("P1","%Z' s. s=(setlocs Z newlocs)[Loc Arg ::= fun Z]")] (hoare_derivs.Call RS conseq1), etac conseq12] 7); @@ -335,7 +335,7 @@ by (fast_tac (claset() addDs [WT_bodiesD]) 2); by (Clarsimp_tac 1); by (rtac hoare_derivs.asm 1); -by (fast_tac (claset() addIs [domI]) 1); +by (fast_tac (claset() addIs [(thm"domI")]) 1); qed_spec_mp "MGF_lemma2_simult"; (* requires Body, empty, insert, com_det *) @@ -346,7 +346,7 @@ by (Clarsimp_tac 1); by (subgoal_tac "{}||-(%pn. {=}. BODY pn .{->})`dom body" 1); by (etac hoare_derivs.weaken 1); -by (fast_tac (claset() addIs [domI]) 1); +by (fast_tac (claset() addIs [(thm"domI")]) 1); by (rtac (finite_dom_body RSN (2,MGT_Body)) 1); by (Simp_tac 1); by (eatac MGF_lemma2_simult 1 1);