diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Bali/DefiniteAssignment.thy
--- a/src/HOL/Bali/DefiniteAssignment.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -1350,18 +1350,18 @@
   from da  
   show "\<And> B'. B \<subseteq> B' \<Longrightarrow> \<exists> A'. Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" (is "PROP ?Hyp Env B t")
   proof (induct) 
-    case Skip thus ?case by (rules intro: da.Skip)
+    case Skip thus ?case by (iprover intro: da.Skip)
   next
-    case Expr thus ?case by (rules intro: da.Expr)
+    case Expr thus ?case by (iprover intro: da.Expr)
   next
     case (Lab A B C Env c l B')  
     have "PROP ?Hyp Env B \<langle>c\<rangle>" .
     moreover
     have B': "B \<subseteq> B'" .
     ultimately obtain C' where "Env\<turnstile> B' \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
-      by rules
+      by iprover
     then obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Break l\<bullet> c\<rangle>\<guillemotright> A'"
-      by (rules intro: da.Lab)
+      by (iprover intro: da.Lab)
     thus ?case ..
   next
     case (Comp A B C1 C2 Env c1 c2 B')
@@ -1370,7 +1370,7 @@
     moreover
     have B': "B \<subseteq> B'" .
     ultimately obtain C1' where da_c1': "Env\<turnstile> B' \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
-      by rules
+      by iprover
     with da_c1 B'
     have
       "nrm C1 \<subseteq> nrm C1'"
@@ -1378,9 +1378,9 @@
     moreover
     have "PROP ?Hyp Env (nrm C1) \<langle>c2\<rangle>" .
     ultimately obtain C2' where "Env\<turnstile> nrm C1' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
-      by rules
+      by iprover
     with da_c1' obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1;; c2\<rangle>\<guillemotright> A'"
-      by (rules intro: da.Comp)
+      by (iprover intro: da.Comp)
     thus ?case ..
   next
     case (If A B C1 C2 E Env c1 c2 e B')
@@ -1389,7 +1389,7 @@
     proof -
       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule If.hyps)
       with B'  
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover
     obtain C1' where "Env\<turnstile> (B' \<union> assigns_if True e) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'"
@@ -1400,7 +1400,7 @@
       moreover
       have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c1\<rangle>" by (rule If.hyps)
       ultimately 
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover
     obtain C2' where "Env\<turnstile> (B' \<union> assigns_if False e) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
@@ -1410,11 +1410,11 @@
       moreover
       have "PROP ?Hyp Env (B \<union> assigns_if False e) \<langle>c2\<rangle>" by (rule If.hyps)
       ultimately
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     ultimately
     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>If(e) c1 Else c2\<rangle>\<guillemotright> A'"
-      by (rules intro: da.If)
+      by (iprover intro: da.If)
     thus ?case ..
   next  
     case (Loop A B C E Env c e l B')
@@ -1423,7 +1423,7 @@
     proof -
       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Loop.hyps)
       with B'  
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover
     obtain C' where "Env\<turnstile> (B' \<union> assigns_if True e) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'"
@@ -1434,11 +1434,11 @@
       moreover
       have "PROP ?Hyp Env (B \<union> assigns_if True e) \<langle>c\<rangle>" by (rule Loop.hyps)
       ultimately 
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     ultimately
     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>l\<bullet> While(e) c\<rangle>\<guillemotright> A'"
-      by (rules intro: da.Loop )
+      by (iprover intro: da.Loop )
     thus ?case ..
   next
     case (Jmp A B Env jump B') 
@@ -1453,12 +1453,12 @@
                                 | Cont l \<Rightarrow> \<lambda>k. UNIV
                                 | Ret \<Rightarrow> \<lambda>k. UNIV)"
                      
-      by  rules
+      by  iprover
     ultimately have "Env\<turnstile> B' \<guillemotright>\<langle>Jmp jump\<rangle>\<guillemotright> A'"
       by (rule da.Jmp)
     thus ?case ..
   next
-    case Throw thus ?case by (rules intro: da.Throw )
+    case Throw thus ?case by (iprover intro: da.Throw )
   next
     case (Try A B C C1 C2 Env c1 c2 vn B')
     have B': "B \<subseteq> B'" .
@@ -1466,7 +1466,7 @@
     proof -
       have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Try.hyps)
       with B'  
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover
     obtain C2' where 
@@ -1478,11 +1478,11 @@
                       (B \<union> {VName vn}) \<langle>c2\<rangle>" 
 	by (rule Try.hyps)
       ultimately
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     ultimately
     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>Try c1 Catch(C vn) c2\<rangle>\<guillemotright> A'"
-      by (rules intro: da.Try )
+      by (iprover intro: da.Try )
     thus ?case ..
   next
     case (Fin A B C1 C2 Env c1 c2 B')
@@ -1491,33 +1491,33 @@
     proof -
       have "PROP ?Hyp Env B \<langle>c1\<rangle>" by (rule Fin.hyps)
       with B'  
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover
     obtain C2' where "Env\<turnstile> B' \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'"
     proof -
       have "PROP ?Hyp Env B \<langle>c2\<rangle>" by (rule Fin.hyps)
       with B'
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     ultimately
     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c1 Finally c2\<rangle>\<guillemotright> A'"
-      by (rules intro: da.Fin )
+      by (iprover intro: da.Fin )
     thus ?case ..
   next
-    case Init thus ?case by (rules intro: da.Init)
+    case Init thus ?case by (iprover intro: da.Init)
   next
-    case NewC thus ?case by (rules intro: da.NewC)
+    case NewC thus ?case by (iprover intro: da.NewC)
   next
-    case NewA thus ?case by (rules intro: da.NewA)
+    case NewA thus ?case by (iprover intro: da.NewA)
   next
-    case Cast thus ?case by (rules intro: da.Cast)
+    case Cast thus ?case by (iprover intro: da.Cast)
   next
-    case Inst thus ?case by (rules intro: da.Inst)
+    case Inst thus ?case by (iprover intro: da.Inst)
   next
-    case Lit thus ?case by (rules intro: da.Lit)
+    case Lit thus ?case by (iprover intro: da.Lit)
   next
-    case UnOp thus ?case by (rules intro: da.UnOp)
+    case UnOp thus ?case by (iprover intro: da.UnOp)
   next
     case (CondAnd A B E1 E2 Env e1 e2 B')
     have B': "B \<subseteq> B'" .
@@ -1525,7 +1525,7 @@
     proof -
       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondAnd.hyps)
       with B'  
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover
     obtain E2' where "Env\<turnstile> B' \<union>  assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
@@ -1534,11 +1534,11 @@
 	by blast
       moreover
       have "PROP ?Hyp Env (B \<union> assigns_if True e1) \<langle>e2\<rangle>" by (rule CondAnd.hyps)
-      ultimately show ?thesis using that by rules
+      ultimately show ?thesis using that by iprover
     qed
     ultimately
     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondAnd e1 e2\<rangle>\<guillemotright> A'"
-      by (rules intro: da.CondAnd)
+      by (iprover intro: da.CondAnd)
     thus ?case ..
   next
     case (CondOr A B E1 E2 Env e1 e2 B')
@@ -1547,7 +1547,7 @@
     proof -
       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule CondOr.hyps)
       with B'  
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover
     obtain E2' where "Env\<turnstile> B' \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
@@ -1556,11 +1556,11 @@
 	by blast
       moreover
       have "PROP ?Hyp Env (B \<union> assigns_if False e1) \<langle>e2\<rangle>" by (rule CondOr.hyps)
-      ultimately show ?thesis using that by rules
+      ultimately show ?thesis using that by iprover
     qed
     ultimately
     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>BinOp CondOr e1 e2\<rangle>\<guillemotright> A'"
-      by (rules intro: da.CondOr)
+      by (iprover intro: da.CondOr)
     thus ?case ..
   next
     case (BinOp A B E1 Env binop e1 e2 B')
@@ -1569,7 +1569,7 @@
     proof -
       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule BinOp.hyps)
       with B'  
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover
     obtain A' where "Env\<turnstile> nrm E1' \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'"
@@ -1580,35 +1580,35 @@
 	by (rule da_monotone [THEN conjE])
       moreover 
       have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule BinOp.hyps)
-      ultimately show ?thesis using that by rules
+      ultimately show ?thesis using that by iprover
     qed
     ultimately
     have "Env\<turnstile> B' \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<guillemotright> A'"
-      using BinOp.hyps by (rules intro: da.BinOp)
+      using BinOp.hyps by (iprover intro: da.BinOp)
     thus ?case ..
   next
     case (Super B Env B')
     have B': "B \<subseteq> B'" .
     with Super.hyps have "This \<in> B' "
       by auto
-    thus ?case by (rules intro: da.Super)
+    thus ?case by (iprover intro: da.Super)
   next
     case (AccLVar A B Env vn B')
     have "vn \<in> B" .
     moreover
     have "B \<subseteq> B'" .
     ultimately have "vn \<in> B'" by auto
-    thus ?case by (rules intro: da.AccLVar)
+    thus ?case by (iprover intro: da.AccLVar)
   next
-    case Acc thus ?case by (rules intro: da.Acc)
+    case Acc thus ?case by (iprover intro: da.Acc)
   next 
     case (AssLVar A B E Env e vn B')
     have B': "B \<subseteq> B'" .
     then obtain E' where "Env\<turnstile> B' \<guillemotright>\<langle>e\<rangle>\<guillemotright> E'"
-      by (rule AssLVar.hyps [elim_format]) rules
+      by (rule AssLVar.hyps [elim_format]) iprover
     then obtain A' where  
       "Env\<turnstile> B' \<guillemotright>\<langle>LVar vn:=e\<rangle>\<guillemotright> A'"
-      by (rules intro: da.AssLVar)
+      by (iprover intro: da.AssLVar)
     thus ?case ..
   next
     case (Ass A B Env V e v B') 
@@ -1619,7 +1619,7 @@
     proof -
       have "PROP ?Hyp Env B \<langle>v\<rangle>" by (rule Ass.hyps)
       with B'  
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover
     obtain A' where "Env\<turnstile> nrm V' \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'"
@@ -1630,11 +1630,11 @@
 	by (rule da_monotone [THEN conjE])
       moreover 
       have "PROP ?Hyp Env (nrm V) \<langle>e\<rangle>" by (rule Ass.hyps)
-      ultimately show ?thesis using that by rules
+      ultimately show ?thesis using that by iprover
     qed  
     ultimately
     have "Env\<turnstile> B' \<guillemotright>\<langle>v := e\<rangle>\<guillemotright> A'"
-      by (rules intro: da.Ass)
+      by (iprover intro: da.Ass)
     thus ?case ..
   next
     case (CondBool A B C E1 E2 Env c e1 e2 B')
@@ -1644,7 +1644,7 @@
     proof -
       have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule CondBool.hyps)
       with B'  
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover 
     obtain E1' where "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
@@ -1655,7 +1655,7 @@
       moreover
       have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule CondBool.hyps)
       ultimately 
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover
     obtain E2' where "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
@@ -1666,11 +1666,11 @@
       moreover
       have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by(rule CondBool.hyps)
       ultimately 
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     ultimately 
     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'"
-      by (rules intro: da.CondBool)
+      by (iprover intro: da.CondBool)
     thus ?case ..
   next
     case (Cond A B C E1 E2 Env c e1 e2 B')
@@ -1680,7 +1680,7 @@
     proof -
       have "PROP ?Hyp Env B \<langle>c\<rangle>" by (rule Cond.hyps)
       with B'  
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover 
     obtain E1' where "Env\<turnstile> B' \<union> assigns_if True c \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'"
@@ -1691,7 +1691,7 @@
       moreover
       have "PROP ?Hyp Env (B \<union> assigns_if True c) \<langle>e1\<rangle>" by (rule Cond.hyps)
       ultimately 
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover
     obtain E2' where "Env\<turnstile> B' \<union> assigns_if False c \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'"
@@ -1702,11 +1702,11 @@
       moreover
       have "PROP ?Hyp Env (B \<union> assigns_if False c) \<langle>e2\<rangle>" by (rule Cond.hyps)
       ultimately 
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     ultimately 
     obtain A' where "Env\<turnstile> B' \<guillemotright>\<langle>c ? e1 : e2\<rangle>\<guillemotright> A'"
-      by (rules intro: da.Cond)
+      by (iprover intro: da.Cond)
     thus ?case ..
   next
     case (Call A B E Env accC args e mn mode pTs statT B')
@@ -1715,7 +1715,7 @@
     proof -
       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Call.hyps)
       with B'  
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover
     obtain A' where "Env\<turnstile> nrm E' \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'"
@@ -1726,14 +1726,14 @@
 	by (rule da_monotone [THEN conjE])
       moreover 
       have "PROP ?Hyp Env (nrm E) \<langle>args\<rangle>" by (rule Call.hyps)
-      ultimately show ?thesis using that by rules
+      ultimately show ?thesis using that by iprover
     qed  
     ultimately
     have "Env\<turnstile> B' \<guillemotright>\<langle>{accC,statT,mode}e\<cdot>mn( {pTs}args)\<rangle>\<guillemotright> A'"
-      by (rules intro: da.Call)
+      by (iprover intro: da.Call)
     thus ?case ..
   next
-    case Methd thus ?case by (rules intro: da.Methd)
+    case Methd thus ?case by (iprover intro: da.Methd)
   next
     case (Body A B C D Env c B')  
     have B': "B \<subseteq> B'" .
@@ -1747,7 +1747,7 @@
       ultimately
       have "nrm C \<subseteq> nrm C'"
 	by (rule da_monotone [THEN conjE])
-      with da_c that show ?thesis by rules
+      with da_c that show ?thesis by iprover
     qed
     moreover 
     have "Result \<in> nrm C" .
@@ -1756,12 +1756,12 @@
     moreover have "jumpNestingOkS {Ret} c" .
     ultimately obtain A' where
       "Env\<turnstile> B' \<guillemotright>\<langle>Body D c\<rangle>\<guillemotright> A'"
-      by (rules intro: da.Body)
+      by (iprover intro: da.Body)
     thus ?case ..
   next
-    case LVar thus ?case by (rules intro: da.LVar)
+    case LVar thus ?case by (iprover intro: da.LVar)
   next
-    case FVar thus ?case by (rules intro: da.FVar)
+    case FVar thus ?case by (iprover intro: da.FVar)
   next
     case (AVar A B E1 Env e1 e2 B')
     have B': "B \<subseteq> B'" .
@@ -1769,7 +1769,7 @@
     proof -
       have "PROP ?Hyp Env B \<langle>e1\<rangle>" by (rule AVar.hyps)
       with B'  
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover
     obtain A' where "Env\<turnstile> nrm E1' \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'"
@@ -1780,14 +1780,14 @@
 	by (rule da_monotone [THEN conjE])
       moreover 
       have "PROP ?Hyp Env (nrm E1) \<langle>e2\<rangle>" by (rule AVar.hyps)
-      ultimately show ?thesis using that by rules
+      ultimately show ?thesis using that by iprover
     qed  
     ultimately
     have "Env\<turnstile> B' \<guillemotright>\<langle>e1.[e2]\<rangle>\<guillemotright> A'"
-      by (rules intro: da.AVar)
+      by (iprover intro: da.AVar)
     thus ?case ..
   next
-    case Nil thus ?case by (rules intro: da.Nil)
+    case Nil thus ?case by (iprover intro: da.Nil)
   next
     case (Cons A B E Env e es B')
     have B': "B \<subseteq> B'" .
@@ -1795,7 +1795,7 @@
     proof -
       have "PROP ?Hyp Env B \<langle>e\<rangle>" by (rule Cons.hyps)
       with B'  
-      show ?thesis using that by rules
+      show ?thesis using that by iprover
     qed
     moreover
     obtain A' where "Env\<turnstile> nrm E' \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'"
@@ -1806,11 +1806,11 @@
 	by (rule da_monotone [THEN conjE])
       moreover 
       have "PROP ?Hyp Env (nrm E) \<langle>es\<rangle>" by (rule Cons.hyps)
-      ultimately show ?thesis using that by rules
+      ultimately show ?thesis using that by iprover
     qed  
     ultimately
     have "Env\<turnstile> B' \<guillemotright>\<langle>e # es\<rangle>\<guillemotright> A'"
-      by (rules intro: da.Cons)
+      by (iprover intro: da.Cons)
     thus ?case ..
   qed
 qed
@@ -1841,13 +1841,13 @@
 proof -
   from da B'
   obtain A' where A': "Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'"
-    by (rule da_weaken [elim_format]) rules
+    by (rule da_weaken [elim_format]) iprover
   with da B'
   have "nrm A \<subseteq> nrm A' \<and> (\<forall> l. brk A l \<subseteq> brk A' l)"
     by (rule da_monotone)
   with A' ex_mono
   show ?thesis
-    by rules
+    by iprover
 qed
 
-end
\ No newline at end of file
+end