# 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);