# HG changeset patch
# User nipkow
# Date 1127426175 -7200
# Node ID 58eeffd73be1953bd4d558d2d47d89d2b17d915e
# Parent  f2bd501398eef6940492e9a0ba33e45b6a7691f5
renamed rules to iprover

diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/AxCompl.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -451,9 +451,9 @@
 	  proof -
 	    from eval_e wt_e da_e wf normal_s1
 	    have "nrm C \<subseteq>  dom (locals (store s1))"
-	      by (cases rule: da_good_approxE') rules
+	      by (cases rule: da_good_approxE') iprover
 	    with da_ps show ?thesis
-	      by (rule da_weakenE) rules
+	      by (rule da_weakenE) iprover
 	  qed
 	}
 	ultimately show ?thesis
@@ -845,7 +845,7 @@
 	  show ?thesis
 	    by (rule eval_type_soundE)
 	qed
-	ultimately show ?thesis by rules
+	ultimately show ?thesis by iprover
       qed
     qed
   next
@@ -1528,7 +1528,7 @@
     proof -
       from eval_t type_ok wf 
       obtain n where evaln: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (Y', s')"
-	by (rule eval_to_evaln [elim_format]) rules
+	by (rule eval_to_evaln [elim_format]) iprover
       from valid have 
 	valid_expanded:
 	"\<forall>n Y s Z. P Y s Z \<longrightarrow> type_ok G t s 
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/AxSound.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -192,7 +192,7 @@
   from evaln have "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)"
     by (rule evaln_eval)
   from this wt da wf elim show P
-    by (rule da_good_approxE') rules+
+    by (rule da_good_approxE') iprover+
 qed
 
 lemma validI: 
@@ -336,7 +336,7 @@
 proof -
   from evaln have "G\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" by (rule evaln_eval)
   from this hyps show ?thesis
-    by (rule dom_locals_eval_mono_elim) rules+
+    by (rule dom_locals_eval_mono_elim) iprover+
 qed
 
 
@@ -616,7 +616,7 @@
 	proof -
 	  from eval_e1  wt_e1 da_e1 wf True
 	  have "nrm E1 \<subseteq> dom (locals (store s1))"
-	    by (cases rule: da_good_approx_evalnE) rules
+	    by (cases rule: da_good_approx_evalnE) iprover
 	  with da_e2 show ?thesis
 	    by (rule da_weakenE)
 	qed
@@ -944,7 +944,7 @@
 	obtain E2 where
 	  da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
                    \<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
-	  by (rule da_e2_BinOp [elim_format]) rules
+	  by (rule da_e2_BinOp [elim_format]) iprover
 	from wt_e2 wt_Skip obtain T2 
 	  where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
                   \<turnstile>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<Colon>T2"
@@ -957,7 +957,7 @@
 	case False
 	note ve=validE [OF valid_e2,OF Q' valid_A conf_s1 eval_e2]
 	with False show ?thesis
-	  by rules
+	  by iprover
       qed
       with v have "R \<lfloor>v\<rfloor>\<^sub>e s2 Z"
 	by simp
@@ -1068,7 +1068,7 @@
 	  proof -
 	    from eval_var wt_var da_var wf True
 	    have "nrm V \<subseteq>  dom (locals (store s1))"
-	      by (cases rule: da_good_approx_evalnE) rules
+	      by (cases rule: da_good_approx_evalnE) iprover
 	    with da_e show ?thesis
 	      by (rule da_weakenE) 
 	  qed
@@ -1079,7 +1079,7 @@
 	  case False
 	  note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e]
 	  with False show ?thesis
-	    by rules
+	    by iprover
 	qed
 	with s3 show "R \<lfloor>v\<rfloor>\<^sub>e s3 Z"
 	  by simp
@@ -1120,7 +1120,7 @@
 	  case False
 	  note ve=validE [OF valid_e,OF Q' valid_A conf_s1 eval_e]
 	  with False show ?thesis
-	    by rules
+	    by iprover
 	qed
 	with s3 show "R \<lfloor>v\<rfloor>\<^sub>e s3 Z"
 	  by simp
@@ -1213,7 +1213,7 @@
 	case False
 	with valid_then_else P' valid_A conf_s1 eval_then_else
 	show ?thesis
-	  by (cases rule: validE) rules+
+	  by (cases rule: validE) iprover+
       qed
       moreover
       from eval wt da conf_s0 wf
@@ -1308,7 +1308,7 @@
 	proof -
 	  from evaln_e wt_e da_e wf True
 	  have "nrm C \<subseteq>  dom (locals (store s1))"
-	    by (cases rule: da_good_approx_evalnE) rules
+	    by (cases rule: da_good_approx_evalnE) iprover
 	  with da_args show ?thesis
 	    by (rule da_weakenE) 
 	qed
@@ -1328,7 +1328,7 @@
 	case False
 	with valid_args Q valid_A conf_s1 evaln_args
 	obtain "(R a) \<lfloor>vs\<rfloor>\<^sub>l s2 Z" "s2\<Colon>\<preceq>(G,L)" 
-	  by (cases rule: validE) rules+
+	  by (cases rule: validE) iprover+
 	moreover
 	from False evaln_args have "s2=s1"
 	  by auto
@@ -1413,7 +1413,7 @@
 	proof -
 	  from evaln_e wt_e da_e wf normal_s1
 	  have "nrm C \<subseteq>  dom (locals (store s1))"
-	    by (cases rule: da_good_approx_evalnE) rules
+	    by (cases rule: da_good_approx_evalnE) iprover
 	  with da_args show ?thesis
 	    by (rule da_weakenE) 
 	qed
@@ -1545,7 +1545,7 @@
                ,lcl=callee_lcl invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> (mthd dynM)
                \<rparr> \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'" and
               res: "Result \<in> nrm M'"
-	      by (rule wf_mdeclE) rules
+	      by (rule wf_mdeclE) iprover
 	    from da_body is_static_eq L' have
 	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
                  \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'"
@@ -1594,7 +1594,7 @@
 	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> \<turnstile> dom (locals (store s3')) 
                      \<guillemotright>\<langle>Body (declclass dynM) (stmt (mbody (mthd dynM)))\<rangle>\<guillemotright> M3"
 	      using da
-	      by (rules intro: da.Body assigned.select_convs)
+	      by (iprover intro: da.Body assigned.select_convs)
 	    from _ this [simplified]
 	    show ?thesis
 	      by (rule da.Methd [simplified,elim_format])
@@ -1602,12 +1602,12 @@
 	  qed
 	  from valid_methd R' valid_A conf_s3' evaln_methd wt_methd da_methd
 	  have "(set_lvars l .; S) \<lfloor>v\<rfloor>\<^sub>e s4 Z"
-	    by (cases rule: validE) rules+
+	    by (cases rule: validE) iprover+
 	  with s5 l show ?thesis
 	    by simp
 	qed
       qed
-      with conf_s5 show ?thesis by rules
+      with conf_s5 show ?thesis by iprover
     qed
   qed
 next
@@ -1755,7 +1755,7 @@
 	proof -
 	  from eval_e wt_e da_e wf True
 	  have "nrm E1 \<subseteq> dom (locals (store s1))"
-	    by (cases rule: da_good_approx_evalnE) rules
+	    by (cases rule: da_good_approx_evalnE) iprover
 	  with da_es show ?thesis
 	    by (rule da_weakenE)
 	qed
@@ -1766,7 +1766,7 @@
 	case False
 	with valid_es Q' valid_A conf_s1 eval_es 
 	show ?thesis
-	  by (cases rule: validE) rules+
+	  by (cases rule: validE) iprover+
       qed
       with v have "R \<lfloor>v\<rfloor>\<^sub>l s2 Z"
 	by simp
@@ -1904,7 +1904,7 @@
 	proof -
 	  from eval_c1 wt_c1 da_c1 wf True
 	  have "nrm C1 \<subseteq> dom (locals (store s1))"
-	    by (cases rule: da_good_approx_evalnE) rules
+	    by (cases rule: da_good_approx_evalnE) iprover
 	  with da_c2 show ?thesis
 	    by (rule da_weakenE)
 	qed
@@ -1915,7 +1915,7 @@
 	case False
 	from valid_c2 Q valid_A conf_s1 eval_c2 False
 	show ?thesis
-	  by (cases rule: validE) rules+
+	  by (cases rule: validE) iprover+
       qed
       moreover
       from eval wt da conf_s0 wf
@@ -1992,7 +1992,7 @@
 	case False
 	with valid_then_else P' valid_A conf_s1 eval_then_else
 	show ?thesis
-	  by (cases rule: validE) rules+
+	  by (cases rule: validE) iprover+
       qed
       moreover
       from eval wt da conf_s0 wf
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/Decl.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -80,7 +80,7 @@
     have "\<forall> x y. x < (y::acc_modi) \<and> y < x \<longrightarrow> False"
       by (auto simp add: less_acc_def split add: acc_modi.split)
     with prems show ?thesis
-      by (unfold le_acc_def) rules
+      by (unfold le_acc_def) iprover
   qed
   next
   show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
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
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -165,7 +165,7 @@
   qed (simp_all)
   with jumpNestingOk_l' subset
   show ?thesis
-    by rules
+    by iprover
 qed
    
 corollary jumpNestingOk_mono: 
@@ -429,7 +429,7 @@
             by simp
           moreover from jmp_s1 have "?Jmp ({Cont l} \<union> jmps) s1" by simp
           ultimately have jmp_s2: "?Jmp ({Cont l} \<union> jmps) s2" 
-            using wt_c G by rules
+            using wt_c G by iprover
           have "?Jmp jmps (abupd (absorb (Cont l)) s2)"
           proof -
             {
@@ -1701,7 +1701,7 @@
 	by - (erule halloc_no_abrupt [rule_format])
       hence "normal s2" by (cases s2) simp
       with NewA.hyps
-      show ?thesis by rules
+      show ?thesis by iprover
     qed
     also
     from halloc 
@@ -1732,7 +1732,7 @@
     hence "normal s1" by - (erule eval_no_abrupt_lemma [rule_format]) 
     with BinOp.hyps
     have "assigns (In1l e1) \<subseteq> dom (locals (store s1))"
-      by rules
+      by iprover
     also
     have "\<dots>  \<subseteq> dom (locals (store s2))"
     proof -
@@ -1768,7 +1768,7 @@
       by - (erule eval_no_abrupt_lemma [rule_format]) 
     with Ass.hyps
     have "assigns (In2 va) \<subseteq> dom (locals (store s1))" 
-      by rules
+      by iprover
     also
     from Ass.hyps
     have "\<dots> \<subseteq> dom (locals (store s2))"
@@ -1776,7 +1776,7 @@
     also
     from nrm_s2 Ass.hyps
     have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
-      by rules
+      by iprover
     ultimately
     have "assigns (In2 va) \<union> assigns (In1l e) \<subseteq>  dom (locals (store s2))"
       by (rule Un_least)
@@ -1816,7 +1816,7 @@
       by - (erule eval_no_abrupt_lemma [rule_format])
     with Cond.hyps
     have "assigns (In1l e0) \<subseteq> dom (locals (store s1))"
-      by rules
+      by iprover
     also from Cond.hyps
     have "\<dots> \<subseteq> dom (locals (store s2))"
       by - (erule dom_locals_eval_mono_elim)
@@ -1868,14 +1868,14 @@
       by - (erule eval_no_abrupt_lemma [rule_format])
     with Call.hyps
     have "assigns (In1l e) \<subseteq> dom (locals (store s1))"
-      by rules
+      by iprover
     also from Call.hyps
     have "\<dots> \<subseteq>  dom (locals (store s2))"
       by - (erule dom_locals_eval_mono_elim)
     also
     from nrm_s2 Call.hyps
     have "assigns (In3 args) \<subseteq> dom (locals (store s2))"
-      by rules
+      by iprover
     ultimately have "assigns (In1l e) \<union> assigns (In3 args) \<subseteq> \<dots>"
       by (rule Un_least)
     also 
@@ -1903,7 +1903,7 @@
     qed
     with FVar.hyps 
     have "assigns (In1l e) \<subseteq> dom (locals (store s2))"
-      by rules
+      by iprover
     also
     have "\<dots> \<subseteq>  dom (locals (store s2'))"
     proof -
@@ -1932,14 +1932,14 @@
       by - (erule eval_no_abrupt_lemma [rule_format])
     with AVar.hyps
     have "assigns (In1l e1) \<subseteq> dom (locals (store s1))"
-      by rules
+      by iprover
     also from AVar.hyps
     have "\<dots> \<subseteq>  dom (locals (store s2))"
       by - (erule dom_locals_eval_mono_elim)
     also
     from AVar.hyps nrm_s2
     have "assigns (In1l e2) \<subseteq> dom (locals (store s2))"
-      by rules
+      by iprover
     ultimately
     have "assigns (In1l e1) \<union> assigns (In1l e2) \<subseteq> \<dots>"
       by (rule Un_least)
@@ -1962,14 +1962,14 @@
     proof -
       from Cons
       have "normal s1" by - (erule eval_no_abrupt_lemma [rule_format])
-      with Cons.hyps show ?thesis by rules
+      with Cons.hyps show ?thesis by iprover
     qed
     also from Cons.hyps
     have "\<dots> \<subseteq>  dom (locals (store s2))"
       by - (erule dom_locals_eval_mono_elim)
     also from Cons
     have "assigns (In3 es) \<subseteq> dom (locals (store s2))"
-      by rules
+      by iprover
     ultimately
     have "assigns (In1l e) \<union> assigns (In3 es) \<subseteq> dom (locals (store s2))"
       by (rule Un_least)
@@ -2043,7 +2043,7 @@
       by cases simp
     from ce ve
     obtain eq_ve_ce: "ve=ce" and nrm_s: "normal s"
-      by (rule UnOp.hyps [elim_format]) rules
+      by (rule UnOp.hyps [elim_format]) iprover
     from eq_ve_ce const ce v 
     have "v=c" 
       by simp
@@ -2066,7 +2066,7 @@
     from c1 v1
     obtain eq_v1_c1: "v1 = c1" and 
              nrm_s1: "normal s1"
-      by (rule BinOp.hyps [elim_format]) rules
+      by (rule BinOp.hyps [elim_format]) iprover
     show ?case
     proof (cases "need_second_arg binop v1")
       case True
@@ -2074,7 +2074,7 @@
 	where "G\<turnstile>Norm s1' \<midarrow>e2-\<succ>v2\<rightarrow> s" 
 	by (cases s1) simp
       with c2 obtain "v2 = c2" "normal s"
-	by (rule BinOp.hyps [elim_format]) rules
+	by (rule BinOp.hyps [elim_format]) iprover
       with c c1 c2 eq_v1_c1 v 
       show ?thesis by simp
     next
@@ -2111,7 +2111,7 @@
       by cases simp 
     from cb vb
     obtain eq_vb_cb: "vb = cb" and nrm_s1: "normal s1"
-      by (rule Cond.hyps [elim_format]) rules 
+      by (rule Cond.hyps [elim_format]) iprover 
     show ?case
     proof (cases "the_Bool vb")
       case True
@@ -2123,7 +2123,7 @@
 	where "G\<turnstile>Norm s1' \<midarrow>e1-\<succ>v\<rightarrow> s"
 	by (cases s1) simp
       with c1 obtain "c1 = v" "normal s"
-	by (rule Cond.hyps [elim_format]) rules 
+	by (rule Cond.hyps [elim_format]) iprover 
       ultimately show ?thesis by simp
     next
       case False
@@ -2135,7 +2135,7 @@
 	where "G\<turnstile>Norm s1' \<midarrow>e2-\<succ>v\<rightarrow> s"
 	by (cases s1) simp
       with c2 obtain "c2 = v" "normal s"
-	by (rule Cond.hyps [elim_format]) rules 
+	by (rule Cond.hyps [elim_format]) iprover 
       ultimately show ?thesis by simp
     qed
   next
@@ -2143,7 +2143,7 @@
   qed simp_all
   with const eval
   show ?thesis
-    by rules
+    by iprover
 qed
   
 lemmas constVal_eval_elim = constVal_eval [THEN conjE]
@@ -2235,7 +2235,7 @@
   qed simp_all
   with const wt
   show ?thesis
-    by rules
+    by iprover
 qed	
       
 lemma assigns_if_good_approx:
@@ -2777,12 +2777,12 @@
     show ?case
     proof (cases "normal s1")
       case True
-      with nrm_c1 have "nrm C1 \<subseteq> dom (locals (snd s1))" by rules
+      with nrm_c1 have "nrm C1 \<subseteq> dom (locals (snd s1))" by iprover
       with da_c2 obtain C2' 
 	where  da_c2': "Env\<turnstile> dom (locals (snd s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
                nrm_c2: "nrm C2 \<subseteq> nrm C2'"                  and
                brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"
-        by (rule da_weakenE) rules
+        by (rule da_weakenE) iprover
       have "PROP ?Hyp (In1r c2) s1 s2" .
       with wt_c2 da_c2' G
       obtain nrm_c2': "?NormalAssigned s2 C2'" and 
@@ -2871,7 +2871,7 @@
 	  where da_c1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c1\<rangle>\<guillemotright> C1'" and
 	        nrm_c1: "nrm C1 \<subseteq> nrm C1'"                  and
                 brk_c1: "\<forall> l. brk C1 l \<subseteq> brk C1' l"
-          by (rule da_weakenE) rules
+          by (rule da_weakenE) iprover
 	from If.hyps True have "PROP ?Hyp (In1r c1) s1 s2" by simp
 	with wt_c1 da_c1'
 	obtain nrm_c1': "?NormalAssigned s2 C1'" and 
@@ -2901,7 +2901,7 @@
 	  where da_c2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<guillemotright> C2'" and
 	        nrm_c2: "nrm C2 \<subseteq> nrm C2'"                  and
                 brk_c2: "\<forall> l. brk C2 l \<subseteq> brk C2' l"
-          by (rule da_weakenE) rules
+          by (rule da_weakenE) iprover
 	from If.hyps False have "PROP ?Hyp (In1r c2) s1 s2" by simp
 	with wt_c2 da_c2'
 	obtain nrm_c2': "?NormalAssigned s2 C2'" and 
@@ -2993,7 +2993,7 @@
 	  where da_c': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c\<rangle>\<guillemotright> C'" and
 	     nrm_C_C': "nrm C \<subseteq> nrm C'"                  and
              brk_C_C': "\<forall> l. brk C l \<subseteq> brk C' l"
-          by (rule da_weakenE) rules
+          by (rule da_weakenE) iprover
 	from hyp_c wt_c da_c'
 	obtain nrm_C': "?NormalAssigned s2 C'" and 
           brk_C': "?BreakAssigned s1 s2 C'" and
@@ -3855,11 +3855,11 @@
           with wt_e1 da_e1 G normal_s1
           obtain "?NormalAssigned s1 E1"  
             by simp
-          with normal_s1 have "nrm E1 \<subseteq> dom (locals (store s1))" by rules
+          with normal_s1 have "nrm E1 \<subseteq> dom (locals (store s1))" by iprover
           with da_e2 obtain A' 
             where  da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and
                  nrm_A_A': "nrm A \<subseteq> nrm A'"                  
-            by (rule da_weakenE) rules
+            by (rule da_weakenE) iprover
           from notAndOr have "need_second_arg binop v1" by simp
           with BinOp.hyps 
           have "PROP ?Hyp (In1l e2) s1 s2" by simp
@@ -4004,7 +4004,7 @@
         with da_e obtain A' 
           where  da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and
                  nrm_A_A': "nrm A \<subseteq> nrm A'"                  
-          by (rule da_weakenE) rules
+          by (rule da_weakenE) iprover
         from hyp_e wt_e da_e' G normal_s2
         obtain "nrm A' \<subseteq> dom (locals (store s2))"   
           by simp
@@ -4121,7 +4121,7 @@
           with da_e1 obtain E1' where
                   da_e1': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e1\<rangle>\<guillemotright> E1'" and
               nrm_E1_E1': "nrm E1 \<subseteq> nrm E1'"
-            by (rule da_weakenE) rules
+            by (rule da_weakenE) iprover
           ultimately have "nrm E1' \<subseteq> dom (locals (store s2))"
             using wt_e1 G normal_s2 by simp 
           with nrm_E1_E1' show ?thesis
@@ -4140,7 +4140,7 @@
           with da_e2 obtain E2' where
                   da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> E2'" and
               nrm_E2_E2': "nrm E2 \<subseteq> nrm E2'"
-            by (rule da_weakenE) rules
+            by (rule da_weakenE) iprover
           ultimately have "nrm E2' \<subseteq> dom (locals (store s2))"
             using wt_e2 G normal_s2 by simp 
           with nrm_E2_E2' show ?thesis
@@ -4206,7 +4206,7 @@
         with da_args obtain A' where
           da_args': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>args\<rangle>\<guillemotright> A'" and
           nrm_A_A': "nrm A \<subseteq> nrm A'"
-          by (rule da_weakenE) rules
+          by (rule da_weakenE) iprover
         have "PROP ?Hyp (In3 args) s1 s2" .
         with da_args' wt_args G normal_s2
         have "nrm A' \<subseteq> dom (locals (store s2))"
@@ -4313,7 +4313,7 @@
         with da_e obtain A' where
           da_e': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e\<rangle>\<guillemotright> A'" and
           nrm_A_A': "nrm A \<subseteq> nrm A'"
-          by (rule da_weakenE) rules
+          by (rule da_weakenE) iprover
         have normal_s2: "normal s2"
         proof -
           from normal_s3 s3 
@@ -4391,7 +4391,7 @@
         with da_e2 obtain A' where
           da_e2': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>e2\<rangle>\<guillemotright> A'" and
           nrm_A_A': "nrm A \<subseteq> nrm A'"
-          by (rule da_weakenE) rules
+          by (rule da_weakenE) iprover
         have "PROP ?Hyp (In1l e2) s1 s2" .
         with da_e2' wt_e2 G normal_s2
         have "nrm A' \<subseteq> dom (locals (store s2))"
@@ -4459,7 +4459,7 @@
         with da_es obtain A' where
           da_es': "Env\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>es\<rangle>\<guillemotright> A'" and
           nrm_A_A': "nrm A \<subseteq> nrm A'"
-          by (rule da_weakenE) rules
+          by (rule da_weakenE) iprover
         have "PROP ?Hyp (In3 es) s1 s2" .
         with da_es' wt_es G normal_s2
         have "nrm A' \<subseteq> dom (locals (store s2))"
@@ -4523,10 +4523,10 @@
   moreover note wt da
   moreover from wf have "wf_prog (prg \<lparr>prg=G,cls=C,lcl=L\<rparr>)" by simp
   ultimately show ?thesis
-    using elim by (rule da_good_approxE) rules+
+    using elim by (rule da_good_approxE) iprover+
 qed
 
 ML {*
 Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
 *}
-end
\ No newline at end of file
+end
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Bali/Eval.thy
--- a/src/HOL/Bali/Eval.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/Eval.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -192,7 +192,7 @@
 defer 
 apply (case_tac "a' = Null")
 apply  simp_all
-apply rules
+apply iprover
 done
 
 constdefs
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Bali/Evaln.thy
--- a/src/HOL/Bali/Evaln.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/Evaln.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -554,7 +554,7 @@
   case (Abrupt s t xc)
   obtain n where
     "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, Some xc, s)"
-    by (rules intro: evaln.Abrupt)
+    by (iprover intro: evaln.Abrupt)
   then show ?case ..
 next
   case Skip
@@ -563,7 +563,7 @@
   case (Expr e s0 s1 v)
   then obtain n where
     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
-    by (rules)
+    by (iprover)
   then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
     by (rule evaln.Expr) 
   then show ?case ..
@@ -571,7 +571,7 @@
   case (Lab c l s0 s1)
   then obtain n where
     "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
-    by (rules)
+    by (iprover)
   then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
     by (rule evaln.Lab)
   then show ?case ..
@@ -580,7 +580,7 @@
   then obtain n1 n2 where
     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
     "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
-    by (rules)
+    by (iprover)
   then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
     by (blast intro: evaln.Comp dest: evaln_max2 )
   then show ?case ..
@@ -589,7 +589,7 @@
   then obtain n1 n2 where
     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
     "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
-    by (rules)
+    by (iprover)
   then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
     by (blast intro: evaln.If dest: evaln_max2)
   then show ?case ..
@@ -597,18 +597,18 @@
   case (Loop b c e l s0 s1 s2 s3)
   from Loop.hyps obtain n1 where
     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
-    by (rules)
+    by (iprover)
   moreover from Loop.hyps obtain n2 where
     "if the_Bool b 
         then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
               G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
 	else s3 = s1"
-    by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
+    by simp (iprover intro: evaln_nonstrict le_maxI1 le_maxI2)
   ultimately
   have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
     apply -
     apply (rule evaln.Loop)
-    apply   (rules intro: evaln_nonstrict intro: le_maxI1)
+    apply   (iprover intro: evaln_nonstrict intro: le_maxI1)
 
     apply   (auto intro: evaln_nonstrict intro: le_maxI2)
     done
@@ -622,7 +622,7 @@
   case (Throw a e s0 s1)
   then obtain n where
     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
-    by (rules)
+    by (iprover)
   then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
     by (rule evaln.Throw)
   then show ?case ..
@@ -630,7 +630,7 @@
   case (Try catchC c1 c2 s0 s1 s2 s3 vn)
   from Try.hyps obtain n1 where
     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
-    by (rules)
+    by (iprover)
   moreover 
   have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
   moreover
@@ -646,7 +646,7 @@
   from Fin obtain n1 n2 where 
     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
     "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
-    by rules
+    by iprover
   moreover
   have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
                      then (x1, s1)
@@ -673,17 +673,17 @@
   case (NewC C a s0 s1 s2)
   then obtain n where 
     "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
-    by (rules)
+    by (iprover)
   with NewC 
   have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
-    by (rules intro: evaln.NewC)
+    by (iprover intro: evaln.NewC)
   then show ?case ..
 next
   case (NewA T a e i s0 s1 s2 s3)
   then obtain n1 n2 where 
     "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
     "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
-    by (rules)
+    by (iprover)
   moreover
   have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
   ultimately
@@ -694,7 +694,7 @@
   case (Cast castT e s0 s1 s2 v)
   then obtain n where
     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
-    by (rules)
+    by (iprover)
   moreover 
   have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
   ultimately
@@ -705,7 +705,7 @@
   case (Inst T b e s0 s1 v)
   then obtain n where
     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
-    by (rules)
+    by (iprover)
   moreover 
   have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
   ultimately
@@ -721,7 +721,7 @@
   case (UnOp e s0 s1 unop v )
   then obtain n where
     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
-    by (rules)
+    by (iprover)
   hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
     by (rule evaln.UnOp)
   then show ?case ..
@@ -731,7 +731,7 @@
     "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
     "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
                else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"    
-    by (rules)
+    by (iprover)
   hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
           \<rightarrow> s2"
     by (blast intro!: evaln.BinOp dest: evaln_max2)
@@ -749,7 +749,7 @@
   case (Acc f s0 s1 v va)
   then obtain n where
     "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
-    by (rules)
+    by (iprover)
   then
   have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
     by (rule evaln.Acc)
@@ -759,7 +759,7 @@
   then obtain n1 n2 where 
     "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
     "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"      
-    by (rules)
+    by (iprover)
   then
   have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
     by (blast intro: evaln.Ass dest: evaln_max2)
@@ -769,7 +769,7 @@
   then obtain n1 n2 where 
     "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
     "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
-    by (rules)
+    by (iprover)
   then
   have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
     by (blast intro: evaln.Cond dest: evaln_max2)
@@ -780,7 +780,7 @@
   then obtain n1 n2 where
     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
     "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
-    by rules
+    by iprover
   moreover
   have "invDeclC = invocation_declclass G mode (store s2) a' statT 
                        \<lparr>name=mn,parTs=pTs'\<rparr>" .
@@ -792,7 +792,7 @@
   from Call.hyps
   obtain m where 
     "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
-    by rules
+    by iprover
   ultimately
   have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
             (set_lvars (locals (store s2))) s4"
@@ -802,7 +802,7 @@
   case (Methd D s0 s1 sig v )
   then obtain n where
     "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
-    by rules
+    by iprover
   then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
     by (rule evaln.Methd)
   then show ?case ..
@@ -811,7 +811,7 @@
   from Body.hyps obtain n1 n2 where 
     evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
     evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
-    by (rules)
+    by (iprover)
   moreover
   have "s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
                      fst s2 = Some (Jump (Cont l))
@@ -821,33 +821,33 @@
   have
      "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
        \<rightarrow> abupd (absorb Ret) s3"
-    by (rules intro: evaln.Body dest: evaln_max2)
+    by (iprover intro: evaln.Body dest: evaln_max2)
   then show ?case ..
 next
   case (LVar s vn )
   obtain n where
     "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
-    by (rules intro: evaln.LVar)
+    by (iprover intro: evaln.LVar)
   then show ?case ..
 next
   case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v)
   then obtain n1 n2 where
     "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
     "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
-    by rules
+    by iprover
   moreover
   have "s3 = check_field_access G accC statDeclC fn stat a s2'" 
        "(v, s2') = fvar statDeclC stat fn a s2" .
   ultimately
   have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
-    by (rules intro: evaln.FVar dest: evaln_max2)
+    by (iprover intro: evaln.FVar dest: evaln_max2)
   then show ?case ..
 next
   case (AVar a e1 e2 i s0 s1 s2 s2' v )
   then obtain n1 n2 where 
     "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
     "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
-    by rules
+    by iprover
   moreover 
   have "(v, s2') = avar G i a s2" .
   ultimately 
@@ -856,13 +856,13 @@
   then show ?case ..
 next
   case (Nil s0)
-  show ?case by (rules intro: evaln.Nil)
+  show ?case by (iprover intro: evaln.Nil)
 next
   case (Cons e es s0 s1 s2 v vs)
   then obtain n1 n2 where 
     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
     "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"      
-    by rules
+    by iprover
   then
   have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
     by (blast intro!: evaln.Cons dest: evaln_max2)
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -1233,7 +1233,7 @@
   next
     case (Cons y ys')
     have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
-      by (rules intro: Hyps map_upd_cong_ext)
+      by (iprover intro: Hyps map_upd_cong_ext)
     with Cons show ?thesis
       by simp
   qed
@@ -1701,7 +1701,7 @@
 	  by cases simp+
 	from eval_e1 wt_e1 da_e1 wf normal_s1 
 	have "nrm E1' \<subseteq> dom (locals (store s1))"
-	  by (cases rule: da_good_approxE') rules
+	  by (cases rule: da_good_approxE') iprover
 	with da_e2 show ?thesis
 	  using that by (rule da_weakenE) (simp add: True)
       qed
@@ -1836,7 +1836,7 @@
       proof -
 	from eval_c1 wt_c1 da_c1 wf True
 	have "nrm C1 \<subseteq> dom (locals (store s1))"
-	  by (cases rule: da_good_approxE') rules
+	  by (cases rule: da_good_approxE') iprover
 	with da_c2 show ?thesis
 	  by (rule da_weakenE)
       qed
@@ -2806,7 +2806,7 @@
 	proof -
 	  from eval_var wt_var da_var wf normal_s1
 	  have "nrm V \<subseteq>  dom (locals (store s1))"
-	    by (cases rule: da_good_approxE') rules
+	    by (cases rule: da_good_approxE') iprover
 	  with da_e show ?thesis
 	    by (rule da_weakenE) 
 	qed
@@ -3094,7 +3094,7 @@
       proof -
 	from eval_e wt_e da_e wf normal_s1
 	have "nrm E \<subseteq>  dom (locals (store s1))"
-	  by (cases rule: da_good_approxE') rules
+	  by (cases rule: da_good_approxE') iprover
 	with da_args show ?thesis
 	  by (rule da_weakenE) 
       qed
@@ -3256,7 +3256,7 @@
                ,lcl=callee_lcl invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> (mthd dynM)
                \<rparr> \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'" and
               res: "Result \<in> nrm M'"
-	      by (rule wf_mdeclE) rules
+	      by (rule wf_mdeclE) iprover
 	    from da_body is_static_eq L' have
 	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
                  \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'"
@@ -3308,7 +3308,7 @@
 	      "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> \<turnstile> dom (locals (store s3')) 
                      \<guillemotright>\<langle>Body (declclass dynM) (stmt (mbody (mthd dynM)))\<rangle>\<guillemotright> M3"
 	      using da
-	      by (rules intro: da.Body assigned.select_convs)
+	      by (iprover intro: da.Body assigned.select_convs)
 	    from _ this [simplified]
 	    show ?thesis
 	      by (rule da.Methd [simplified,elim_format])
@@ -3672,7 +3672,7 @@
       proof -
 	from eval_e1 wt_e1 da_e1 wf True
 	have "nrm E1 \<subseteq> dom (locals (store s1))"
-	  by (cases rule: da_good_approxE') rules
+	  by (cases rule: da_good_approxE') iprover
 	with da_e2 show ?thesis
 	  by (rule da_weakenE)
       qed
@@ -3768,7 +3768,7 @@
       proof -
 	from eval_e wt_e da_e wf True
 	have "nrm E \<subseteq> dom (locals (store s1))"
-	  by (cases rule: da_good_approxE') rules
+	  by (cases rule: da_good_approxE') iprover
 	with da_es show ?thesis
 	  by (rule da_weakenE)
       qed
@@ -3806,7 +3806,7 @@
                   error_free s0 = error_free s1\<rbrakk> \<Longrightarrow> P"
   shows "P"
 using eval wt da wf conf
-by (rule eval_type_sound [elim_format]) (rules intro: elim) 
+by (rule eval_type_sound [elim_format]) (iprover intro: elim) 
 
  
 corollary eval_ts: 
@@ -3995,19 +3995,19 @@
 	proof -
 	  from eval_c1 wt_c1 da_c1 wf normal_s1
 	  have "nrm C1 \<subseteq> dom (locals (store s1))"
-	    by (cases rule: da_good_approxE') rules
+	    by (cases rule: da_good_approxE') iprover
 	  with da_c2 show ?thesis
 	    by (rule da_weakenE)
 	qed
 	with wt_c2 have "P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2"
 	  by (rule Comp.hyps)
 	with da show ?thesis
-	  using elim by rules
+	  using elim by iprover
       qed
     }
     with eval_c1 eval_c2 wt_c1 wt_c2 da_c1 P_c1 
     show ?case
-      by (rule comp) rules+
+      by (rule comp) iprover+
   next
     case (If b c1 c2 e s0 s1 s2 L accC T A)
     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
@@ -4058,12 +4058,12 @@
 	with wt_then_else
 	have "P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2"
 	  by (rule If.hyps)
-	with da show ?thesis using elim by rules
+	with da show ?thesis using elim by iprover
       qed
     }
     with eval_e eval_then_else wt_e wt_then_else da_e P_e
     show ?case
-      by (rule if) rules+
+      by (rule if) iprover+
   next
     oops
 
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Datatype_Universe.thy
--- a/src/HOL/Datatype_Universe.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Datatype_Universe.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -218,17 +218,17 @@
 
 lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'"
 apply (erule equalityE)
-apply (rules intro: equalityI Scons_inject_lemma1)
+apply (iprover intro: equalityI Scons_inject_lemma1)
 done
 
 lemma Scons_inject2: "Scons M N = Scons M' N' ==> N=N'"
 apply (erule equalityE)
-apply (rules intro: equalityI Scons_inject_lemma2)
+apply (iprover intro: equalityI Scons_inject_lemma2)
 done
 
 lemma Scons_inject:
     "[| Scons M N = Scons M' N';  [| M=M';  N=N' |] ==> P |] ==> P"
-by (rules dest: Scons_inject1 Scons_inject2)
+by (iprover dest: Scons_inject1 Scons_inject2)
 
 lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' & N=N')"
 by (blast elim!: Scons_inject)
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Equiv_Relations.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -35,7 +35,7 @@
   apply (unfold equiv_def)
   apply clarify
   apply (rule equalityI)
-   apply (rules intro: sym_trans_comp_subset refl_comp_subset)+
+   apply (iprover intro: sym_trans_comp_subset refl_comp_subset)+
   done
 
 text {* Second half. *}
@@ -73,7 +73,7 @@
 
 lemma eq_equiv_class:
     "r``{a} = r``{b} ==> equiv A r ==> b \<in> A ==> (a, b) \<in> r"
-  by (rules intro: equalityD2 subset_equiv_class)
+  by (iprover intro: equalityD2 subset_equiv_class)
 
 lemma equiv_class_nondisjoint:
     "equiv A r ==> x \<in> (r``{a} \<inter> r``{b}) ==> (a, b) \<in> r"
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -604,7 +604,7 @@
 	  have "finite A" by(rule foldSet_imp_finite[OF Afoldx])
 	  with AbB have "finite ?D" by simp
 	  then obtain d where Dfoldd: "(?D,d) \<in> foldSet f g z"
-	    using finite_imp_foldSet by rules
+	    using finite_imp_foldSet by iprover
 	  moreover have cinB: "c \<in> B" using B by auto
 	  ultimately have "(B,g c \<cdot> d) \<in> foldSet f g z"
 	    by(rule Diff1_foldSet)
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/FixedPoint.thy
--- a/src/HOL/FixedPoint.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/FixedPoint.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -31,13 +31,13 @@
 by (auto simp add: lfp_def)
 
 lemma lfp_lemma2: "mono(f) ==> f(lfp(f)) \<subseteq> lfp(f)"
-by (rules intro: lfp_greatest subset_trans monoD lfp_lowerbound)
+by (iprover intro: lfp_greatest subset_trans monoD lfp_lowerbound)
 
 lemma lfp_lemma3: "mono(f) ==> lfp(f) \<subseteq> f(lfp(f))"
-by (rules intro: lfp_lemma2 monoD lfp_lowerbound)
+by (iprover intro: lfp_lemma2 monoD lfp_lowerbound)
 
 lemma lfp_unfold: "mono(f) ==> lfp(f) = f(lfp(f))"
-by (rules intro: equalityI lfp_lemma2 lfp_lemma3)
+by (iprover intro: equalityI lfp_lemma2 lfp_lemma3)
 
 subsection{*General induction rules for greatest fixed points*}
 
@@ -105,13 +105,13 @@
 by (auto simp add: gfp_def)
 
 lemma gfp_lemma2: "mono(f) ==> gfp(f) \<subseteq> f(gfp(f))"
-by (rules intro: gfp_least subset_trans monoD gfp_upperbound)
+by (iprover intro: gfp_least subset_trans monoD gfp_upperbound)
 
 lemma gfp_lemma3: "mono(f) ==> f(gfp(f)) \<subseteq> gfp(f)"
-by (rules intro: gfp_lemma2 monoD gfp_upperbound)
+by (iprover intro: gfp_lemma2 monoD gfp_upperbound)
 
 lemma gfp_unfold: "mono(f) ==> gfp(f) = f(gfp(f))"
-by (rules intro: equalityI gfp_lemma2 gfp_lemma3)
+by (iprover intro: equalityI gfp_lemma2 gfp_lemma3)
 
 subsection{*Coinduction rules for greatest fixed points*}
 
@@ -141,7 +141,7 @@
   @{term lfp} and @{term gfp}*}
 
 lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)"
-by (rules intro: subset_refl monoI Un_mono monoD)
+by (iprover intro: subset_refl monoI Un_mono monoD)
 
 lemma coinduct3_lemma:
      "[| X \<subseteq> f(lfp(%x. f(x) Un X Un gfp(f)));  mono(f) |]
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Fun.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -429,11 +429,11 @@
 proof 
   assume "inj_on (swap a b f) A"
   with A have "inj_on (swap a b (swap a b f)) A" 
-    by (rules intro: inj_on_imp_inj_on_swap) 
+    by (iprover intro: inj_on_imp_inj_on_swap) 
   thus "inj_on f A" by simp 
 next
   assume "inj_on f A"
-  with A show "inj_on (swap a b f) A" by (rules intro: inj_on_imp_inj_on_swap)
+  with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
 qed
 
 lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/HOL.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -287,7 +287,7 @@
 subsection {*Equality of booleans -- iff*}
 
 lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q"
-apply (rules intro: iff [THEN mp, THEN mp] impI prems)
+apply (iprover intro: iff [THEN mp, THEN mp] impI prems)
 done
 
 lemma iffD2: "[| P=Q; Q |] ==> P"
@@ -307,7 +307,7 @@
   assumes major: "P=Q"
       and minor: "[| P --> Q; Q --> P |] ==> R"
   shows "R"
-by (rules intro: minor impI major [THEN iffD2] major [THEN iffD1])
+by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])
 
 
 subsection {*True*}
@@ -318,7 +318,7 @@
 done
 
 lemma eqTrueI: "P ==> P=True"
-by (rules intro: iffI TrueI)
+by (iprover intro: iffI TrueI)
 
 lemma eqTrueE: "P=True ==> P"
 apply (erule iffD2)
@@ -330,7 +330,7 @@
 
 lemma allI: assumes p: "!!x::'a. P(x)" shows "ALL x. P(x)"
 apply (unfold All_def)
-apply (rules intro: ext eqTrueI p)
+apply (iprover intro: ext eqTrueI p)
 done
 
 lemma spec: "ALL x::'a. P(x) ==> P(x)"
@@ -343,13 +343,13 @@
   assumes major: "ALL x. P(x)"
       and minor: "P(x) ==> R"
   shows "R"
-by (rules intro: minor major [THEN spec])
+by (iprover intro: minor major [THEN spec])
 
 lemma all_dupE:
   assumes major: "ALL x. P(x)"
       and minor: "[| P(x); ALL x. P(x) |] ==> R"
   shows "R"
-by (rules intro: minor major major [THEN spec])
+by (iprover intro: minor major major [THEN spec])
 
 
 subsection {*False*}
@@ -370,7 +370,7 @@
   assumes p: "P ==> False"
   shows "~P"
 apply (unfold not_def)
-apply (rules intro: impI p)
+apply (iprover intro: impI p)
 done
 
 lemma False_not_True: "False ~= True"
@@ -399,24 +399,24 @@
 lemma impE:
   assumes "P-->Q" "P" "Q ==> R"
   shows "R"
-by (rules intro: prems mp)
+by (iprover intro: prems mp)
 
 (* Reduces Q to P-->Q, allowing substitution in P. *)
 lemma rev_mp: "[| P;  P --> Q |] ==> Q"
-by (rules intro: mp)
+by (iprover intro: mp)
 
 lemma contrapos_nn:
   assumes major: "~Q"
       and minor: "P==>Q"
   shows "~P"
-by (rules intro: notI minor major [THEN notE])
+by (iprover intro: notI minor major [THEN notE])
 
 (*not used at all, but we already have the other 3 combinations *)
 lemma contrapos_pn:
   assumes major: "Q"
       and minor: "P ==> ~Q"
   shows "~P"
-by (rules intro: notI minor major notE)
+by (iprover intro: notI minor major notE)
 
 lemma not_sym: "t ~= s ==> s ~= t"
 apply (erule contrapos_nn)
@@ -436,7 +436,7 @@
 
 lemma exI: "P x ==> EX x::'a. P x"
 apply (unfold Ex_def)
-apply (rules intro: allI allE impI mp)
+apply (iprover intro: allI allE impI mp)
 done
 
 lemma exE:
@@ -444,7 +444,7 @@
       and minor: "!!x. P(x) ==> Q"
   shows "Q"
 apply (rule major [unfolded Ex_def, THEN spec, THEN mp])
-apply (rules intro: impI [THEN allI] minor)
+apply (iprover intro: impI [THEN allI] minor)
 done
 
 
@@ -452,17 +452,17 @@
 
 lemma conjI: "[| P; Q |] ==> P&Q"
 apply (unfold and_def)
-apply (rules intro: impI [THEN allI] mp)
+apply (iprover intro: impI [THEN allI] mp)
 done
 
 lemma conjunct1: "[| P & Q |] ==> P"
 apply (unfold and_def)
-apply (rules intro: impI dest: spec mp)
+apply (iprover intro: impI dest: spec mp)
 done
 
 lemma conjunct2: "[| P & Q |] ==> Q"
 apply (unfold and_def)
-apply (rules intro: impI dest: spec mp)
+apply (iprover intro: impI dest: spec mp)
 done
 
 lemma conjE:
@@ -476,19 +476,19 @@
 
 lemma context_conjI:
   assumes prems: "P" "P ==> Q" shows "P & Q"
-by (rules intro: conjI prems)
+by (iprover intro: conjI prems)
 
 
 subsection {*Disjunction*}
 
 lemma disjI1: "P ==> P|Q"
 apply (unfold or_def)
-apply (rules intro: allI impI mp)
+apply (iprover intro: allI impI mp)
 done
 
 lemma disjI2: "Q ==> P|Q"
 apply (unfold or_def)
-apply (rules intro: allI impI mp)
+apply (iprover intro: allI impI mp)
 done
 
 lemma disjE:
@@ -496,7 +496,7 @@
       and minorP: "P ==> R"
       and minorQ: "Q ==> R"
   shows "R"
-by (rules intro: minorP minorQ impI
+by (iprover intro: minorP minorQ impI
                  major [unfolded or_def, THEN spec, THEN mp, THEN mp])
 
 
@@ -536,7 +536,7 @@
   assumes p1: "Q"
       and p2: "~P ==> ~Q"
   shows "P"
-by (rules intro: classical p1 p2 notE)
+by (iprover intro: classical p1 p2 notE)
 
 
 subsection {*Unique existence*}
@@ -544,14 +544,14 @@
 lemma ex1I:
   assumes prems: "P a" "!!x. P(x) ==> x=a"
   shows "EX! x. P(x)"
-by (unfold Ex1_def, rules intro: prems exI conjI allI impI)
+by (unfold Ex1_def, iprover intro: prems exI conjI allI impI)
 
 text{*Sometimes easier to use: the premises have no shared variables.  Safe!*}
 lemma ex_ex1I:
   assumes ex_prem: "EX x. P(x)"
       and eq: "!!x y. [| P(x); P(y) |] ==> x=y"
   shows "EX! x. P(x)"
-by (rules intro: ex_prem [THEN exE] ex1I eq)
+by (iprover intro: ex_prem [THEN exE] ex1I eq)
 
 lemma ex1E:
   assumes major: "EX! x. P(x)"
@@ -559,7 +559,7 @@
   shows "R"
 apply (rule major [unfolded Ex1_def, THEN exE])
 apply (erule conjE)
-apply (rules intro: minor)
+apply (iprover intro: minor)
 done
 
 lemma ex1_implies_ex: "EX! x. P x ==> EX x. P x"
@@ -586,7 +586,7 @@
 lemma theI:
   assumes "P a" and "!!x. P x ==> x=a"
   shows "P (THE x. P x)"
-by (rules intro: prems the_equality [THEN ssubst])
+by (iprover intro: prems the_equality [THEN ssubst])
 
 lemma theI': "EX! x. P x ==> P (THE x. P x)"
 apply (erule ex1E)
@@ -600,7 +600,7 @@
 lemma theI2:
   assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x"
   shows "Q (THE x. P x)"
-by (rules intro: prems theI)
+by (iprover intro: prems theI)
 
 lemma the1_equality: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
 apply (rule the_equality)
@@ -627,11 +627,11 @@
 lemma disjCI:
   assumes "~Q ==> P" shows "P|Q"
 apply (rule classical)
-apply (rules intro: prems disjI1 disjI2 notI elim: notE)
+apply (iprover intro: prems disjI1 disjI2 notI elim: notE)
 done
 
 lemma excluded_middle: "~P | P"
-by (rules intro: disjCI)
+by (iprover intro: disjCI)
 
 text{*case distinction as a natural deduction rule. Note that @{term "~P"}
    is the second case, not the first.*}
@@ -650,7 +650,7 @@
       and minor: "~P ==> R" "Q ==> R"
   shows "R"
 apply (rule excluded_middle [of P, THEN disjE])
-apply (rules intro: minor major [THEN mp])+
+apply (iprover intro: minor major [THEN mp])+
 done
 
 (*This version of --> elimination works on Q before P.  It works best for
@@ -661,7 +661,7 @@
       and minor: "Q ==> R" "~P ==> R"
   shows "R"
 apply (rule excluded_middle [of P, THEN disjE])
-apply (rules intro: minor major [THEN mp])+
+apply (iprover intro: minor major [THEN mp])+
 done
 
 (*Classical <-> elimination. *)
@@ -670,14 +670,14 @@
       and minor: "[| P; Q |] ==> R"  "[| ~P; ~Q |] ==> R"
   shows "R"
 apply (rule major [THEN iffE])
-apply (rules intro: minor elim: impCE notE)
+apply (iprover intro: minor elim: impCE notE)
 done
 
 lemma exCI:
   assumes "ALL x. ~P(x) ==> P(a)"
   shows "EX x. P(x)"
 apply (rule ccontr)
-apply (rules intro: prems exI allI notI notE [of "\<exists>x. P x"])
+apply (iprover intro: prems exI allI notI notE [of "\<exists>x. P x"])
 done
 
 
@@ -949,10 +949,10 @@
     "!!P. (EX x. t=x & P(x)) = P(t)"
     "!!P. (ALL x. x=t --> P(x)) = P(t)"
     "!!P. (ALL x. t=x --> P(x)) = P(t)"
-  by (blast, blast, blast, blast, blast, rules+)
+  by (blast, blast, blast, blast, blast, iprover+)
 
 lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
-  by rules
+  by iprover
 
 lemma ex_simps:
   "!!P Q. (EX x. P x & Q)   = ((EX x. P x) & Q)"
@@ -962,7 +962,7 @@
   "!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)"
   "!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))"
   -- {* Miniscoping: pushing in existential quantifiers. *}
-  by (rules | blast)+
+  by (iprover | blast)+
 
 lemma all_simps:
   "!!P Q. (ALL x. P x & Q)   = ((ALL x. P x) & Q)"
@@ -972,7 +972,7 @@
   "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
   "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
   -- {* Miniscoping: pushing in universal quantifiers. *}
-  by (rules | blast)+
+  by (iprover | blast)+
 
 lemma disj_absorb: "(A | A) = A"
   by blast
@@ -989,28 +989,28 @@
 lemma eq_ac:
   shows eq_commute: "(a=b) = (b=a)"
     and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))"
-    and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (rules, blast+)
-lemma neq_commute: "(a~=b) = (b~=a)" by rules
+    and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+)
+lemma neq_commute: "(a~=b) = (b~=a)" by iprover
 
 lemma conj_comms:
   shows conj_commute: "(P&Q) = (Q&P)"
-    and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by rules+
-lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by rules
+    and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+
+lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover
 
 lemma disj_comms:
   shows disj_commute: "(P|Q) = (Q|P)"
-    and disj_left_commute: "(P|(Q|R)) = (Q|(P|R))" by rules+
-lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by rules
+    and disj_left_commute: "(P|(Q|R)) = (Q|(P|R))" by iprover+
+lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by iprover
 
-lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by rules
-lemma conj_disj_distribR: "((P|Q)&R) = (P&R | Q&R)" by rules
+lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by iprover
+lemma conj_disj_distribR: "((P|Q)&R) = (P&R | Q&R)" by iprover
 
-lemma disj_conj_distribL: "(P|(Q&R)) = ((P|Q) & (P|R))" by rules
-lemma disj_conj_distribR: "((P&Q)|R) = ((P|R) & (Q|R))" by rules
+lemma disj_conj_distribL: "(P|(Q&R)) = ((P|Q) & (P|R))" by iprover
+lemma disj_conj_distribR: "((P&Q)|R) = ((P|R) & (Q|R))" by iprover
 
-lemma imp_conjR: "(P --> (Q&R)) = ((P-->Q) & (P-->R))" by rules
-lemma imp_conjL: "((P&Q) -->R)  = (P --> (Q --> R))" by rules
-lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by rules
+lemma imp_conjR: "(P --> (Q&R)) = ((P-->Q) & (P-->R))" by iprover
+lemma imp_conjL: "((P&Q) -->R)  = (P --> (Q --> R))" by iprover
+lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by iprover
 
 text {* These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}. *}
 lemma imp_disj_not1: "(P --> Q | R) = (~Q --> P --> R)" by blast
@@ -1019,7 +1019,7 @@
 lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" by blast
 lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" by blast
 
-lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by rules
+lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by iprover
 lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" by blast
 lemma not_imp: "(~(P --> Q)) = (P & ~Q)" by blast
 lemma not_iff: "(P~=Q) = (P = (~Q))" by blast
@@ -1028,7 +1028,7 @@
   by blast
 lemma imp_conv_disj: "(P --> Q) = ((~P) | Q)" by blast
 
-lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by rules
+lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by iprover
 
 
 lemma cases_simp: "((P --> Q) & (~P --> Q)) = Q"
@@ -1038,11 +1038,11 @@
 
 lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" by blast
 lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)" by blast
-lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by rules
-lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by rules
+lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by iprover
+lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by iprover
 
-lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by rules
-lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by rules
+lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by iprover
+lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by iprover
 
 text {*
   \medskip The @{text "&"} congruence rule: not included by default!
@@ -1050,11 +1050,11 @@
 
 lemma conj_cong:
     "(P = P') ==> (P' ==> (Q = Q')) ==> ((P & Q) = (P' & Q'))"
-  by rules
+  by iprover
 
 lemma rev_conj_cong:
     "(Q = Q') ==> (Q' ==> (P = P')) ==> ((P & Q) = (P' & Q'))"
-  by rules
+  by iprover
 
 text {* The @{text "|"} congruence rule: not included by default! *}
 
@@ -1063,7 +1063,7 @@
   by blast
 
 lemma eq_sym_conv: "(x = y) = (y = x)"
-  by rules
+  by iprover
 
 
 text {* \medskip if-then-else rules *}
@@ -1109,8 +1109,8 @@
   apply (simplesubst split_if, blast)
   done
 
-lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules
-lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) rules
+lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) iprover
+lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) iprover
 
 text {* \medskip let rules for simproc *}
 
@@ -1285,11 +1285,11 @@
 
 lemma induct_forall_conj: "induct_forall (\<lambda>x. induct_conj (A x) (B x)) =
     induct_conj (induct_forall A) (induct_forall B)"
-  by (unfold induct_forall_def induct_conj_def) rules
+  by (unfold induct_forall_def induct_conj_def) iprover
 
 lemma induct_implies_conj: "induct_implies C (induct_conj A B) =
     induct_conj (induct_implies C A) (induct_implies C B)"
-  by (unfold induct_implies_def induct_conj_def) rules
+  by (unfold induct_implies_def induct_conj_def) iprover
 
 lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)"
 proof
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Induct/PropLog.thy
--- a/src/HOL/Induct/PropLog.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Induct/PropLog.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -236,12 +236,12 @@
 apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]])
  apply (simp add: sat_thms_p, safe)
  txt{*Case @{text"hyps p t-insert(#v,Y) |- p"} *}
- apply (rules intro: thms_excluded_middle_rule 
+ apply (iprover intro: thms_excluded_middle_rule 
 		     insert_Diff_same [THEN weaken_left]
                      insert_Diff_subset2 [THEN weaken_left] 
                      hyps_Diff [THEN Diff_weaken_left])
 txt{*Case @{text"hyps p t-insert(#v -> false,Y) |- p"} *}
- apply (rules intro: thms_excluded_middle_rule 
+ apply (iprover intro: thms_excluded_middle_rule 
 		     insert_Diff_same [THEN weaken_left]
                      insert_Diff_subset2 [THEN weaken_left] 
                      hyps_insert [THEN Diff_weaken_left])
@@ -260,7 +260,7 @@
 theorem completeness [rule_format]: "finite H ==> \<forall>p. H |= p --> H |- p"
 apply (erule finite_induct)
  apply (blast intro: completeness_0)
-apply (rules intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])
+apply (iprover intro: sat_imp thms.H insertI1 weaken_left_insert [THEN thms.MP])
 done
 
 theorem syntax_iff_semantics: "finite H ==> (H |- p) = (H |= p)"
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Integ/Presburger.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -244,10 +244,10 @@
 text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
 
 lemma P_eqtrue: "(P=True) = P"
-  by rules
+  by iprover
 
 lemma P_eqfalse: "(P=False) = (~P)"
-  by rules
+  by iprover
 
 text {*
   \medskip Theorems for the generation of the bachwards direction of
@@ -831,10 +831,10 @@
   by simp
 
 lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
-  by rules
+  by iprover
 
 lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))"
-  by rules
+  by iprover
 
 lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j)))
 ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) "
@@ -952,13 +952,13 @@
   apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
     nat_0_le cong add: conj_cong)
   apply (rule iffI)
-  apply rules
+  apply iprover
   apply (erule exE)
   apply (case_tac "x=0")
   apply (rule_tac x=0 in exI)
   apply simp
   apply (case_tac "0 \<le> k")
-  apply rules
+  apply iprover
   apply (simp add: linorder_not_le)
   apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   apply assumption
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Lambda/Commutation.thy
--- a/src/HOL/Lambda/Commutation.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Lambda/Commutation.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -154,7 +154,7 @@
   proof (rule converse_rtranclE)
     assume "x = b"
     with xc have "(b, c) \<in> R\<^sup>*" by simp
-    thus ?thesis by rules
+    thus ?thesis by iprover
   next
     fix y
     assume xy: "(x, y) \<in> R"
@@ -163,23 +163,23 @@
     proof (rule converse_rtranclE)
       assume "x = c"
       with xb have "(c, b) \<in> R\<^sup>*" by simp
-      thus ?thesis by rules
+      thus ?thesis by iprover
     next
       fix y'
       assume y'c: "(y', c) \<in> R\<^sup>*"
       assume xy': "(x, y') \<in> R"
       with xy have "\<exists>u. (y, u) \<in> R\<^sup>* \<and> (y', u) \<in> R\<^sup>*" by (rule lc)
-      then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by rules
+      then obtain u where yu: "(y, u) \<in> R\<^sup>*" and y'u: "(y', u) \<in> R\<^sup>*" by iprover
       from xy have "(y, x) \<in> R\<inverse>" ..
       from this and yb yu have "\<exists>d. (b, d) \<in> R\<^sup>* \<and> (u, d) \<in> R\<^sup>*" by (rule less)
-      then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by rules
+      then obtain v where bv: "(b, v) \<in> R\<^sup>*" and uv: "(u, v) \<in> R\<^sup>*" by iprover
       from xy' have "(y', x) \<in> R\<inverse>" ..
       moreover from y'u and uv have "(y', v) \<in> R\<^sup>*" by (rule rtrancl_trans)
       moreover note y'c
       ultimately have "\<exists>d. (v, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*" by (rule less)
-      then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by rules
+      then obtain w where vw: "(v, w) \<in> R\<^sup>*" and cw: "(c, w) \<in> R\<^sup>*" by iprover
       from bv vw have "(b, w) \<in> R\<^sup>*" by (rule rtrancl_trans)
-      with cw show ?thesis by rules
+      with cw show ?thesis by iprover
     qed
   qed
 qed
@@ -208,7 +208,7 @@
   proof (rule converse_rtranclE)
     assume "x = b"
     with xc have "(b, c) \<in> R\<^sup>*" by simp
-    thus ?thesis by rules
+    thus ?thesis by iprover
   next
     fix y
     assume xy: "(x, y) \<in> R"
@@ -217,7 +217,7 @@
     proof (rule converse_rtranclE)
       assume "x = c"
       with xb have "(c, b) \<in> R\<^sup>*" by simp
-      thus ?thesis by rules
+      thus ?thesis by iprover
     next
       fix y'
       assume y'c: "(y', c) \<in> R\<^sup>*"
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Lambda/Eta.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -370,7 +370,7 @@
     by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm)
   then have "\<exists>u1 u2 k. s = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1'' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2''" by (rule eta)
   then obtain u1 u2 k where s: "s = eta_expand k (u1 \<degree> u2)"
-    and u1: "u1 \<Rightarrow>\<^sub>\<eta> u1''" and u2: "u2 \<Rightarrow>\<^sub>\<eta> u2''" by rules
+    and u1: "u1 \<Rightarrow>\<^sub>\<eta> u1''" and u2: "u2 \<Rightarrow>\<^sub>\<eta> u2''" by iprover
   from u1 u2 eta s' have "\<not> free u1 0" and "\<not> free u2 0"
     by (simp_all del: free_par_eta add: free_par_eta [symmetric])
   with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (u1[dummy/0] \<degree> u2[dummy/0])"
@@ -399,7 +399,7 @@
   then obtain u'' where s': "s' = Abs u''"
     by (cases s') (auto simp add: subst_Var free_par_eta [symmetric] split: split_if_asm)
   then have "\<exists>u k. s = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u''" by (rule eta)
-  then obtain u k where s: "s = eta_expand k (Abs u)" and u: "u \<Rightarrow>\<^sub>\<eta> u''" by rules
+  then obtain u k where s: "s = eta_expand k (Abs u)" and u: "u \<Rightarrow>\<^sub>\<eta> u''" by iprover
   from eta u s' have "\<not> free u (Suc 0)"
     by (simp del: free_par_eta add: free_par_eta [symmetric])
   with s have "Abs (s \<degree> Var 0) = eta_expand (Suc k) (Abs (u[lift dummy 0/Suc 0]))"
@@ -481,7 +481,7 @@
     by (blast dest: 2)
   from par_eta_subset_eta t' have "t' -e>> s'''" ..
   with t'' have "t'' -e>> s'''" by (rule rtrancl_trans)
-  with s show ?case by rules
+  with s show ?case by iprover
 qed
 
 theorem eta_postponement:
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Lambda/Type.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -149,7 +149,7 @@
   apply simp
   apply (case_tac "ts @ [t]")
   apply (simp add: types_snoc_eq)+
-  apply rules
+  apply iprover
   done
 
 
@@ -269,7 +269,7 @@
 lemma var_app_typesE: "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow>
   (\<And>Ts. e \<turnstile> Var i : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> P) \<Longrightarrow> P"
   apply (drule var_app_types [of _ _ "[]", simplified])
-  apply (rules intro: typing.Var)+
+  apply (iprover intro: typing.Var)+
   done
 
 lemma abs_typeE: "e \<turnstile> Abs t : T \<Longrightarrow> (\<And>U V. e\<langle>0:U\<rangle> \<turnstile> t : V \<Longrightarrow> P) \<Longrightarrow> P"
@@ -346,7 +346,7 @@
   done
 
 theorem subject_reduction': "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<turnstile> t' : T"
-  by (induct set: rtrancl) (rules intro: subject_reduction)+
+  by (induct set: rtrancl) (iprover intro: subject_reduction)+
 
 
 subsection {* Alternative induction rule for types *}
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -26,7 +26,7 @@
   by (simp add: listall_def)
 
 theorem listall_nil_eq [simp]: "listall P [] = True"
-  by (rules intro: listall_nil)
+  by (iprover intro: listall_nil)
 
 theorem listall_cons: "P x \<Longrightarrow> listall P xs \<Longrightarrow> listall P (x # xs)"
   apply (simp add: listall_def)
@@ -84,14 +84,14 @@
   apply (induct m)
   apply (case_tac n)
   apply (case_tac [3] n)
-  apply (simp only: nat.simps, rules?)+
+  apply (simp only: nat.simps, iprover?)+
   done
 
 lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)"
   apply (induct m)
   apply (case_tac n)
   apply (case_tac [3] n)
-  apply (simp del: simp_thms, rules?)+
+  apply (simp del: simp_thms, iprover?)+
   done
 
 lemma App_NF_D: assumes NF: "Var n \<degree>\<degree> ts \<in> NF"
@@ -125,11 +125,11 @@
   apply (erule NF.App)
   apply (rule_tac m=j and n=x in nat_le_dec [THEN disjE, standard])
   apply simp
-  apply (rules intro: NF.App)
+  apply (iprover intro: NF.App)
   apply simp
-  apply (rules intro: NF.App)
+  apply (iprover intro: NF.App)
   apply simp
-  apply (rules intro: NF.Abs)
+  apply (iprover intro: NF.Abs)
   done
 
 lemma app_Var_NF: "t \<in> NF \<Longrightarrow> \<exists>t'. t \<degree> Var i \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
@@ -199,7 +199,7 @@
 	proof (cases ts)
 	  case Nil
 	  with eq have "(Var x \<degree>\<degree> [])[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* u" by simp
-	  with Nil and uNF show ?thesis by simp rules
+	  with Nil and uNF show ?thesis by simp iprover
 	next
 	  case (Cons a as)
           with appT have "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> (a # as) : T'" by simp
@@ -235,10 +235,10 @@
 	    then obtain bs' where
 	      bsred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) bs \<rightarrow>\<^sub>\<beta>\<^sup>*
 	        Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) bs'"
-	      and bsNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) bs' \<in> NF" by rules
+	      and bsNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) bs' \<in> NF" by iprover
 	    from snoc have "?R b" by simp
-	    with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF" by rules
-	    then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF" by rules
+	    with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF" by iprover
+	    then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF" by iprover
 	    from bsNF have "listall (\<lambda>t. t \<in> NF) (map (\<lambda>t. lift t 0) bs')"
 	      by (rule App_NF_D)
 	    moreover have "lift b' 0 \<in> NF" by (rule lift_NF)
@@ -253,20 +253,20 @@
 	    ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp
 	    thus ?case ..
 	  qed
-	  from App and Cons have "listall ?R as" by simp (rules dest: listall_conj2)
+	  from App and Cons have "listall ?R as" by simp (iprover dest: listall_conj2)
 	  with argsT have "\<exists>as'. ?ex Ts as as'" by (rule as)
 	  then obtain as' where
 	    asred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
 	      Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as'"
-	    and asNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<in> NF" by rules
+	    and asNF: "Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<in> NF" by iprover
 	  from App and Cons have "?R a" by simp
 	  with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> a' \<in> NF"
-	    by rules
-	  then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "a' \<in> NF" by rules
+	    by iprover
+	  then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "a' \<in> NF" by iprover
 	  from uNF have "lift u 0 \<in> NF" by (rule lift_NF)
 	  hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> u' \<in> NF" by (rule app_Var_NF)
 	  then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "u' \<in> NF"
-	    by rules
+	    by iprover
 	  from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> ua \<in> NF"
 	  proof (rule MI1)
 	    have "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
@@ -278,7 +278,7 @@
 	    from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction')
 	  qed
 	  then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "ua \<in> NF"
-	    by rules
+	    by iprover
 	  from ared have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* (lift u 0 \<degree> Var 0)[a'/0]"
 	    by (rule subst_preserves_beta2')
 	  also from ured have "(lift u 0 \<degree> Var 0)[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u'[a'/0]"
@@ -305,7 +305,7 @@
 	    with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction')
 	  qed
 	  then obtain r where rred: "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r"
-	    and rnf: "r \<in> NF" by rules
+	    and rnf: "r \<in> NF" by iprover
 	  from asred have
 	    "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>*
 	    (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0]"
@@ -315,7 +315,7 @@
 	  also note rred
 	  finally have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" .
 	  with rnf Cons eq show ?thesis
-	    by (simp add: map_compose [symmetric] o_def) rules
+	    by (simp add: map_compose [symmetric] o_def) iprover
 	qed
       next
 	assume neq: "x \<noteq> i"
@@ -342,10 +342,10 @@
 	    with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)
 	    then obtain bs' where
 	      bsred: "\<And>x'. Var x' \<degree>\<degree> map (\<lambda>t. t[u/i]) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var x' \<degree>\<degree> bs'"
-	      and bsNF: "\<And>x'. Var x' \<degree>\<degree> bs' \<in> NF" by rules
+	      and bsNF: "\<And>x'. Var x' \<degree>\<degree> bs' \<in> NF" by iprover
 	    from snoc have "?R b" by simp
-	    with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF" by rules
-	    then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF" by rules
+	    with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> b' \<in> NF" by iprover
+	    then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "b' \<in> NF" by iprover
 	    from bsred bred have "\<And>x'. (Var x' \<degree>\<degree> map (\<lambda>t. t[u/i]) bs) \<degree> b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>*
               (Var x' \<degree>\<degree> bs') \<degree> b'" by (rule rtrancl_beta_App)
 	    moreover from bsNF [of 0] have "listall (\<lambda>t. t \<in> NF) bs'"
@@ -355,16 +355,16 @@
 	    ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp
 	    thus ?case ..
 	  qed
-	  from App have "listall ?R ts" by (rules dest: listall_conj2)
+	  from App have "listall ?R ts" by (iprover dest: listall_conj2)
 	  with argsT have "\<exists>ts'. ?ex Ts ts ts'" by (rule ts)
 	  then obtain ts' where NF: "?ex Ts ts ts'" ..
 	  from nat_le_dec show ?thesis
 	  proof
 	    assume "i < x"
-	    with NF show ?thesis by simp rules
+	    with NF show ?thesis by simp iprover
 	  next
 	    assume "\<not> (i < x)"
-	    with NF neq show ?thesis by (simp add: subst_Var) rules
+	    with NF neq show ?thesis by (simp add: subst_Var) iprover
 	  qed
 	qed
       qed
@@ -376,7 +376,7 @@
       moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" by (rule lift_type)
       ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" by (rule Abs)
       thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF"
-	by simp (rules intro: rtrancl_beta_Abs NF.Abs)
+	by simp (iprover intro: rtrancl_beta_Abs NF.Abs)
     }
   qed
 qed
@@ -411,15 +411,15 @@
   shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> t' \<in> NF" using T
 proof induct
   case Var
-  show ?case by (rules intro: Var_NF)
+  show ?case by (iprover intro: Var_NF)
 next
   case Abs
-  thus ?case by (rules intro: rtrancl_beta_Abs NF.Abs)
+  thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs)
 next
   case (App T U e s t)
   from App obtain s' t' where
     sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and sNF: "s' \<in> NF"
-    and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "t' \<in> NF" by rules
+    and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "t' \<in> NF" by iprover
   have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> u \<in> NF"
   proof (rule subst_type_NF)
     have "lift t' 0 \<in> NF" by (rule lift_NF)
@@ -438,10 +438,10 @@
     from sred show "e \<turnstile> s' : T \<Rightarrow> U"
       by (rule subject_reduction') (rule rtyping_imp_typing)
   qed
-  then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "u \<in> NF" by simp rules
+  then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "u \<in> NF" by simp iprover
   from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App)
   hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtrancl_trans)
-  with unf show ?case by rules
+  with unf show ?case by iprover
 qed
 
 
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/List.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -264,7 +264,7 @@
 
 lemma length_induct:
 "(!!xs. \<forall>ys. length ys < length xs --> P ys ==> P xs) ==> P xs"
-by (rule measure_induct [of length]) rules
+by (rule measure_induct [of length]) iprover
 
 
 subsubsection {* @{text length} *}
@@ -550,7 +550,7 @@
 by(blast dest:map_injective)
 
 lemma inj_mapI: "inj f ==> inj (map f)"
-by (rules dest: map_injective injD intro: inj_onI)
+by (iprover dest: map_injective injD intro: inj_onI)
 
 lemma inj_mapD: "inj (map f) ==> inj f"
 apply (unfold inj_on_def, clarify)
@@ -977,6 +977,9 @@
 apply (auto split:nat.split)
 done
 
+lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
+by(induct xs)(auto simp:neq_Nil_conv)
+
 
 subsubsection {* @{text take} and @{text drop} *}
 
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/MicroJava/BV/EffectMono.thy
--- a/src/HOL/MicroJava/BV/EffectMono.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/MicroJava/BV/EffectMono.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -78,7 +78,7 @@
       fix n' assume s: "n = Suc n'"
       with l have  "n' \<le> length ls" by simp
       hence "\<exists>a b. ls = a @ b \<and> length a = n'" by (rule Cons [rule_format])
-      then obtain a b where "ls = a @ b" "length a = n'" by rules
+      then obtain a b where "ls = a @ b" "length a = n'" by iprover
       with s have "l # ls = (l#a) @ b \<and> length (l#a) = n" by simp
       thus ?thesis by blast
     qed
@@ -91,9 +91,9 @@
   assume n: "n < length x"
   hence "n \<le> length x" by simp
   hence "\<exists>a b. x = a @ b \<and> length a = n" by (rule append_length_n)
-  then obtain r d where x: "x = r@d" "length r = n" by rules
+  then obtain r d where x: "x = r@d" "length r = n" by iprover
   with n have "\<exists>b c. d = b#c" by (simp add: neq_Nil_conv)
-  then obtain b c where "d = b#c" by rules
+  then obtain b c where "d = b#c" by iprover
   with x have "x = (rev (rev r)) @ b # c \<and> length (rev r) = n" by simp
   thus ?thesis by blast
 qed
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Nat.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -73,7 +73,7 @@
   apply (unfold Zero_nat_def Suc_def)
   apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *}
   apply (erule Rep_Nat [THEN Nat.induct])
-  apply (rules elim: Abs_Nat_inverse [THEN subst])
+  apply (iprover elim: Abs_Nat_inverse [THEN subst])
   done
 
 text {* Distinctness of constructors *}
@@ -128,7 +128,7 @@
   apply (induct n)
   prefer 2
   apply (rule allI)
-  apply (induct_tac x, rules+)
+  apply (induct_tac x, iprover+)
   done
 
 subsection {* Basic properties of "less than" *}
@@ -340,7 +340,7 @@
   by (simp del: less_Suc_eq_le add: less_Suc_eq_le [symmetric] less_Suc_eq)
 
 lemma le_SucE: "m \<le> Suc n ==> (m \<le> n ==> R) ==> (m = Suc n ==> R) ==> R"
-  by (drule le_Suc_eq [THEN iffD1], rules+)
+  by (drule le_Suc_eq [THEN iffD1], iprover+)
 
 lemma Suc_leI: "m < n ==> Suc(m) \<le> n"
   apply (simp add: le_def less_Suc_eq)
@@ -385,7 +385,7 @@
   done
 
 lemma le_eq_less_or_eq: "(m \<le> (n::nat)) = (m < n | m=n)"
-  by (rules intro: less_or_eq_imp_le le_imp_less_or_eq)
+  by (iprover intro: less_or_eq_imp_le le_imp_less_or_eq)
 
 text {* Useful with @{text Blast}. *}
 lemma eq_imp_le: "(m::nat) = n ==> m \<le> n"
@@ -505,7 +505,7 @@
 
 text {* This theorem is useful with @{text blast} *}
 lemma gr0I: "((n::nat) = 0 ==> False) ==> 0 < n"
-  by (rule iffD1, rule neq0_conv, rules)
+  by (rule iffD1, rule neq0_conv, iprover)
 
 lemma gr0_conv_Suc: "(0 < n) = (\<exists>m. n = Suc m)"
   by (fast intro: not0_implies_Suc)
@@ -779,7 +779,7 @@
   by (rule le_less_trans, rule le_add2, rule lessI)
 
 lemma less_iff_Suc_add: "(m < n) = (\<exists>k. n = Suc (m + k))"
-  by (rules intro!: less_add_Suc1 less_imp_Suc_add)
+  by (iprover intro!: less_add_Suc1 less_imp_Suc_add)
 
 lemma trans_le_add1: "(i::nat) \<le> j ==> i \<le> j + m"
   by (rule le_trans, assumption, rule le_add1)
@@ -909,12 +909,12 @@
 lemma zero_induct_lemma: "P k ==> (!!n. P (Suc n) ==> P n) ==> P (k - i)"
   apply (induct k i rule: diff_induct)
   apply (simp_all (no_asm))
-  apply rules
+  apply iprover
   done
 
 lemma zero_induct: "P k ==> (!!n. P (Suc n) ==> P n) ==> P 0"
   apply (rule diff_self_eq_0 [THEN subst])
-  apply (rule zero_induct_lemma, rules+)
+  apply (rule zero_induct_lemma, iprover+)
   done
 
 lemma diff_cancel: "(k + m) - (k + n) = m - (n::nat)"
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Presburger.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -244,10 +244,10 @@
 text {* Theorems to be deleted from simpset when proving simplified formulaes. *}
 
 lemma P_eqtrue: "(P=True) = P"
-  by rules
+  by iprover
 
 lemma P_eqfalse: "(P=False) = (~P)"
-  by rules
+  by iprover
 
 text {*
   \medskip Theorems for the generation of the bachwards direction of
@@ -831,10 +831,10 @@
   by simp
 
 lemma qe_exI: "(!!x::int. A x = B x) ==> (EX (x::int). A(x)) = (EX (x::int). B(x))"
-  by rules
+  by iprover
 
 lemma qe_ALLI: "(!!x::int. A x = B x) ==> (ALL (x::int). A(x)) = (ALL (x::int). B(x))"
-  by rules
+  by iprover
 
 lemma cp_expand: "(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j)))
 ==>(EX (x::int). P (x)) = (EX (j::int) : {1..d}. EX (b::int) : B. (P1 (j) | P(b+j))) "
@@ -952,13 +952,13 @@
   apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
     nat_0_le cong add: conj_cong)
   apply (rule iffI)
-  apply rules
+  apply iprover
   apply (erule exE)
   apply (case_tac "x=0")
   apply (rule_tac x=0 in exI)
   apply simp
   apply (case_tac "0 \<le> k")
-  apply rules
+  apply iprover
   apply (simp add: linorder_not_le)
   apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
   apply assumption
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -405,7 +405,7 @@
         linearformE: "linearform E g"
       and a: "\<forall>x \<in> F. g x = f x"
       and b: "\<forall>x \<in> E. \<bar>g x\<bar> \<le> p x"
-    by (rule abs_HahnBanach [elim_format]) rules
+    by (rule abs_HahnBanach [elim_format]) iprover
 
   txt {* We furthermore have to show that @{text g} is also continuous: *}
 
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Relation.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -70,7 +70,7 @@
   by (simp add: Id_def)
 
 lemma IdE [elim!]: "p : Id ==> (!!x. p = (x, x) ==> P) ==> P"
-  by (unfold Id_def) (rules elim: CollectE)
+  by (unfold Id_def) (iprover elim: CollectE)
 
 lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)"
   by (unfold Id_def) blast
@@ -100,7 +100,7 @@
 lemma diagE [elim!]:
   "c : diag A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
   -- {* The general elimination rule. *}
-  by (unfold diag_def) (rules elim!: UN_E singletonE)
+  by (unfold diag_def) (iprover elim!: UN_E singletonE)
 
 lemma diag_iff: "((x, y) : diag A) = (x = y & x : A)"
   by blast
@@ -117,11 +117,11 @@
 
 lemma rel_compE [elim!]: "xz : r O s ==>
   (!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r  ==> P) ==> P"
-  by (unfold rel_comp_def) (rules elim!: CollectE splitE exE conjE)
+  by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE)
 
 lemma rel_compEpair:
   "(a, c) : r O s ==> (!!y. (a, y) : s ==> (y, c) : r ==> P) ==> P"
-  by (rules elim: rel_compE Pair_inject ssubst)
+  by (iprover elim: rel_compE Pair_inject ssubst)
 
 lemma R_O_Id [simp]: "R O Id = R"
   by fast
@@ -146,7 +146,7 @@
 subsection {* Reflexivity *}
 
 lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"
-  by (unfold refl_def) (rules intro!: ballI)
+  by (unfold refl_def) (iprover intro!: ballI)
 
 lemma reflD: "refl A r ==> a : A ==> (a, a) : r"
   by (unfold refl_def) blast
@@ -156,10 +156,10 @@
 
 lemma antisymI:
   "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
-  by (unfold antisym_def) rules
+  by (unfold antisym_def) iprover
 
 lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
-  by (unfold antisym_def) rules
+  by (unfold antisym_def) iprover
 
 
 subsection {* Symmetry and Transitivity *}
@@ -169,10 +169,10 @@
 
 lemma transI:
   "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
-  by (unfold trans_def) rules
+  by (unfold trans_def) iprover
 
 lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r"
-  by (unfold trans_def) rules
+  by (unfold trans_def) iprover
 
 
 subsection {* Converse *}
@@ -189,7 +189,7 @@
 lemma converseE [elim!]:
   "yx : r^-1 ==> (!!x y. yx = (y, x) ==> (x, y) : r ==> P) ==> P"
     -- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *}
-  by (unfold converse_def) (rules elim!: CollectE splitE bexE)
+  by (unfold converse_def) (iprover elim!: CollectE splitE bexE)
 
 lemma converse_converse [simp]: "(r^-1)^-1 = r"
   by (unfold converse_def) blast
@@ -219,11 +219,11 @@
   by (unfold Domain_def) blast
 
 lemma DomainI [intro]: "(a, b) : r ==> a : Domain r"
-  by (rules intro!: iffD2 [OF Domain_iff])
+  by (iprover intro!: iffD2 [OF Domain_iff])
 
 lemma DomainE [elim!]:
   "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
-  by (rules dest!: iffD1 [OF Domain_iff])
+  by (iprover dest!: iffD1 [OF Domain_iff])
 
 lemma Domain_empty [simp]: "Domain {} = {}"
   by blast
@@ -259,10 +259,10 @@
   by (simp add: Domain_def Range_def)
 
 lemma RangeI [intro]: "(a, b) : r ==> b : Range r"
-  by (unfold Range_def) (rules intro!: converseI DomainI)
+  by (unfold Range_def) (iprover intro!: converseI DomainI)
 
 lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
-  by (unfold Range_def) (rules elim!: DomainE dest!: converseD)
+  by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
 
 lemma Range_empty [simp]: "Range {} = {}"
   by blast
@@ -305,7 +305,7 @@
 
 lemma ImageE [elim!]:
     "b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P"
-  by (unfold Image_def) (rules elim!: CollectE bexE)
+  by (unfold Image_def) (iprover elim!: CollectE bexE)
 
 lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A"
   -- {* This version's more effective when we already have the required @{text a} *}
@@ -334,7 +334,7 @@
   by blast
 
 lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B"
-  by (rules intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
+  by (iprover intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
 
 lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})"
   -- {* NOT suitable for rewriting *}
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Set.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -542,7 +542,7 @@
 
 lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
   -- {* Anti-symmetry of the subset relation. *}
-  by (rules intro: set_ext subsetD)
+  by (iprover intro: set_ext subsetD)
 
 lemmas equalityI [intro!] = subset_antisym
 
@@ -1046,10 +1046,10 @@
 text {* \medskip Big Union -- least upper bound of a set. *}
 
 lemma Union_upper: "B \<in> A ==> B \<subseteq> Union A"
-  by (rules intro: subsetI UnionI)
+  by (iprover intro: subsetI UnionI)
 
 lemma Union_least: "(!!X. X \<in> A ==> X \<subseteq> C) ==> Union A \<subseteq> C"
-  by (rules intro: subsetI elim: UnionE dest: subsetD)
+  by (iprover intro: subsetI elim: UnionE dest: subsetD)
 
 
 text {* \medskip General union. *}
@@ -1058,7 +1058,7 @@
   by blast
 
 lemma UN_least: "(!!x. x \<in> A ==> B x \<subseteq> C) ==> (\<Union>x\<in>A. B x) \<subseteq> C"
-  by (rules intro: subsetI elim: UN_E dest: subsetD)
+  by (iprover intro: subsetI elim: UN_E dest: subsetD)
 
 
 text {* \medskip Big Intersection -- greatest lower bound of a set. *}
@@ -1071,13 +1071,13 @@
   by blast
 
 lemma Inter_greatest: "(!!X. X \<in> A ==> C \<subseteq> X) ==> C \<subseteq> Inter A"
-  by (rules intro: InterI subsetI dest: subsetD)
+  by (iprover intro: InterI subsetI dest: subsetD)
 
 lemma INT_lower: "a \<in> A ==> (\<Inter>x\<in>A. B x) \<subseteq> B a"
   by blast
 
 lemma INT_greatest: "(!!x. x \<in> A ==> C \<subseteq> B x) ==> C \<subseteq> (\<Inter>x\<in>A. B x)"
-  by (rules intro: INT_I subsetI dest: subsetD)
+  by (iprover intro: INT_I subsetI dest: subsetD)
 
 
 text {* \medskip Finite Union -- the least upper bound of two sets. *}
@@ -1809,7 +1809,7 @@
   by blast
 
 lemma distinct_lemma: "f x \<noteq> f y ==> x \<noteq> y"
-  by rules
+  by iprover
 
 
 text {* \medskip Miniscoping: pushing in quantifiers and big Unions
@@ -1955,21 +1955,21 @@
   done
 
 lemma conj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 & P2) --> (Q1 & Q2)"
-  by rules
+  by iprover
 
 lemma disj_mono: "P1 --> Q1 ==> P2 --> Q2 ==> (P1 | P2) --> (Q1 | Q2)"
-  by rules
+  by iprover
 
 lemma imp_mono: "Q1 --> P1 ==> P2 --> Q2 ==> (P1 --> P2) --> (Q1 --> Q2)"
-  by rules
+  by iprover
 
 lemma imp_refl: "P --> P" ..
 
 lemma ex_mono: "(!!x. P x --> Q x) ==> (EX x. P x) --> (EX x. Q x)"
-  by rules
+  by iprover
 
 lemma all_mono: "(!!x. P x --> Q x) ==> (ALL x. P x) --> (ALL x. Q x)"
-  by rules
+  by iprover
 
 lemma Collect_mono: "(!!x. P x --> Q x) ==> Collect P \<subseteq> Collect Q"
   by blast
@@ -1983,10 +1983,10 @@
   ex_mono Collect_mono in_mono
 
 lemma eq_to_mono: "a = b ==> c = d ==> b --> d ==> a --> c"
-  by rules
+  by iprover
 
 lemma eq_to_mono2: "a = b ==> c = d ==> ~ b --> ~ d ==> ~ a --> ~ c"
-  by rules
+  by iprover
 
 lemma Least_mono:
   "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/Transitive_Closure.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -74,8 +74,8 @@
   shows "P b"
 proof -
   from a have "a = a --> P b"
-    by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
-  thus ?thesis by rules
+    by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
+  thus ?thesis by iprover
 qed
 
 lemmas rtrancl_induct2 =
@@ -88,7 +88,7 @@
   fix x y z
   assume "(x, y) \<in> r\<^sup>*"
   assume "(y, z) \<in> r\<^sup>*"
-  thus "(x, z) \<in> r\<^sup>*" by induct (rules!)+
+  thus "(x, z) \<in> r\<^sup>*" by induct (iprover!)+
 qed
 
 lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
@@ -112,7 +112,7 @@
 
 lemma converse_rtrancl_into_rtrancl:
   "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*"
-  by (rule rtrancl_trans) rules+
+  by (rule rtrancl_trans) iprover+
 
 text {*
   \medskip More @{term "r^*"} equations and inclusions.
@@ -158,7 +158,7 @@
   shows "(y, x) \<in> r^*"
 proof -
   from r show ?thesis
-    by induct (rules intro: rtrancl_trans dest!: converseD)+
+    by induct (iprover intro: rtrancl_trans dest!: converseD)+
 qed
 
 theorem rtrancl_converseI:
@@ -166,7 +166,7 @@
   shows "(x, y) \<in> (r^-1)^*"
 proof -
   from r show ?thesis
-    by induct (rules intro: rtrancl_trans converseI)+
+    by induct (iprover intro: rtrancl_trans converseI)+
 qed
 
 lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
@@ -179,7 +179,7 @@
 proof -
   from rtrancl_converseI [OF major]
   show ?thesis
-    by induct (rules intro: cases dest!: converseD rtrancl_converseD)+
+    by induct (iprover intro: cases dest!: converseD rtrancl_converseD)+
 qed
 
 lemmas converse_rtrancl_induct2 =
@@ -197,8 +197,8 @@
   show ?thesis
     apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
      apply (rule_tac [2] major [THEN converse_rtrancl_induct])
-      prefer 2 apply rules
-     prefer 2 apply rules
+      prefer 2 apply iprover
+     prefer 2 apply iprover
     apply (erule asm_rl exE disjE conjE prems)+
     done
 qed
@@ -221,7 +221,7 @@
 lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
   apply (simp only: split_tupled_all)
   apply (erule trancl.induct)
-  apply (rules dest: subsetD)+
+  apply (iprover dest: subsetD)+
   done
 
 lemma r_into_trancl': "!!p. p : r ==> p : r^+"
@@ -232,15 +232,15 @@
 *}
 
 lemma trancl_into_rtrancl: "(a, b) \<in> r^+ ==> (a, b) \<in> r^*"
-  by (erule trancl.induct) rules+
+  by (erule trancl.induct) iprover+
 
 lemma rtrancl_into_trancl1: assumes r: "(a, b) \<in> r^*"
   shows "!!c. (b, c) \<in> r ==> (a, c) \<in> r^+" using r
-  by induct rules+
+  by induct iprover+
 
 lemma rtrancl_into_trancl2: "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+"
   -- {* intro rule from @{text r} and @{text rtrancl} *}
-  apply (erule rtranclE, rules)
+  apply (erule rtranclE, iprover)
   apply (rule rtrancl_trans [THEN rtrancl_into_trancl1])
    apply (assumption | rule r_into_rtrancl)+
   done
@@ -253,8 +253,8 @@
   -- {* Nice induction rule for @{text trancl} *}
 proof -
   from a have "a = a --> P b"
-    by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
-  thus ?thesis by rules
+    by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
+  thus ?thesis by iprover
 qed
 
 lemma trancl_trans_induct:
@@ -267,7 +267,7 @@
   assume major: "(x,y) : r^+"
   case rule_context
   show ?thesis
-    by (rules intro: r_into_trancl major [THEN trancl_induct] prems)
+    by (iprover intro: r_into_trancl major [THEN trancl_induct] prems)
 qed
 
 inductive_cases tranclE: "(a, b) : r^+"
@@ -281,14 +281,14 @@
   fix x y z
   assume "(x, y) \<in> r^+"
   assume "(y, z) \<in> r^+"
-  thus "(x, z) \<in> r^+" by induct (rules!)+
+  thus "(x, z) \<in> r^+" by induct (iprover!)+
 qed
 
 lemmas trancl_trans = trans_trancl [THEN transD, standard]
 
 lemma rtrancl_trancl_trancl: assumes r: "(x, y) \<in> r^*"
   shows "!!z. (y, z) \<in> r^+ ==> (x, z) \<in> r^+" using r
-  by induct (rules intro: trancl_trans)+
+  by induct (iprover intro: trancl_trans)+
 
 lemma trancl_into_trancl2: "(a, b) \<in> r ==> (b, c) \<in> r^+ ==> (a, c) \<in> r^+"
   by (erule transD [OF trans_trancl r_into_trancl])
@@ -309,13 +309,13 @@
 lemma trancl_converseI: "(x, y) \<in> (r^+)^-1 ==> (x, y) \<in> (r^-1)^+"
   apply (drule converseD)
   apply (erule trancl.induct)
-  apply (rules intro: converseI trancl_trans)+
+  apply (iprover intro: converseI trancl_trans)+
   done
 
 lemma trancl_converseD: "(x, y) \<in> (r^-1)^+ ==> (x, y) \<in> (r^+)^-1"
   apply (rule converseI)
   apply (erule trancl.induct)
-  apply (rules dest: converseD intro: trancl_trans)+
+  apply (iprover dest: converseD intro: trancl_trans)+
   done
 
 lemma trancl_converse: "(r^-1)^+ = (r^+)^-1"
diff -r f2bd501398ee -r 58eeffd73be1 src/HOL/ex/Intuitionistic.thy
--- a/src/HOL/ex/Intuitionistic.thy	Thu Sep 22 23:55:42 2005 +0200
+++ b/src/HOL/ex/Intuitionistic.thy	Thu Sep 22 23:56:15 2005 +0200
@@ -24,44 +24,44 @@
 intuitionstically equivalent to P.  [Andy Pitts] *)
 
 lemma "(~~(P&Q)) = ((~~P) & (~~Q))"
-  by rules
+  by iprover
 
 lemma "~~ ((~P --> Q) --> (~P --> ~Q) --> P)"
-  by rules
+  by iprover
 
 (* ~~ does NOT distribute over | *)
 
 lemma "(~~(P-->Q))  = (~~P --> ~~Q)"
-  by rules
+  by iprover
 
 lemma "(~~~P) = (~P)"
-  by rules
+  by iprover
 
 lemma "~~((P --> Q | R)  -->  (P-->Q) | (P-->R))"
-  by rules
+  by iprover
 
 lemma "(P=Q) = (Q=P)"
-  by rules
+  by iprover
 
 lemma "((P --> (Q | (Q-->R))) --> R) --> R"
-  by rules
+  by iprover
 
 lemma "(((G-->A) --> J) --> D --> E) --> (((H-->B)-->I)-->C-->J)
       --> (A-->H) --> F --> G --> (((C-->B)-->I)-->D)-->(A-->C)
       --> (((F-->A)-->B) --> I) --> E"
-  by rules
+  by iprover
 
 
 (* Lemmas for the propositional double-negation translation *)
 
 lemma "P --> ~~P"
-  by rules
+  by iprover
 
 lemma "~~(~~P --> P)"
-  by rules
+  by iprover
 
 lemma "~~P & ~~(P --> Q) --> ~~Q"
-  by rules
+  by iprover
 
 
 (* de Bruijn formulae *)
@@ -70,7 +70,7 @@
 lemma "((P=Q) --> P&Q&R) &
        ((Q=R) --> P&Q&R) &
        ((R=P) --> P&Q&R) --> P&Q&R"
-  by rules
+  by iprover
 
 (*de Bruijn formula with five predicates*)
 lemma "((P=Q) --> P&Q&R&S&T) &
@@ -78,7 +78,7 @@
        ((R=S) --> P&Q&R&S&T) &
        ((S=T) --> P&Q&R&S&T) &
        ((T=P) --> P&Q&R&S&T) --> P&Q&R&S&T"
-  by rules
+  by iprover
 
 
 (*** Problems from Sahlin, Franzen and Haridi, 
@@ -89,81 +89,81 @@
 (*Problem 1.1*)
 lemma "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) =
        (ALL z. EX y. ALL x. p(x) & q(y) & r(z))"
-  by (rules del: allE elim 2: allE')
+  by (iprover del: allE elim 2: allE')
 
 (*Problem 3.1*)
 lemma "~ (EX x. ALL y. p y x = (~ p x x))"
-  by rules
+  by iprover
 
 
 (* Intuitionistic FOL: propositional problems based on Pelletier. *)
 
 (* Problem ~~1 *)
 lemma "~~((P-->Q)  =  (~Q --> ~P))"
-  by rules
+  by iprover
 
 (* Problem ~~2 *)
 lemma "~~(~~P  =  P)"
-  by rules
+  by iprover
 
 (* Problem 3 *)
 lemma "~(P-->Q) --> (Q-->P)"
-  by rules
+  by iprover
 
 (* Problem ~~4 *)
 lemma "~~((~P-->Q)  =  (~Q --> P))"
-  by rules
+  by iprover
 
 (* Problem ~~5 *)
 lemma "~~((P|Q-->P|R) --> P|(Q-->R))"
-  by rules
+  by iprover
 
 (* Problem ~~6 *)
 lemma "~~(P | ~P)"
-  by rules
+  by iprover
 
 (* Problem ~~7 *)
 lemma "~~(P | ~~~P)"
-  by rules
+  by iprover
 
 (* Problem ~~8.  Peirce's law *)
 lemma "~~(((P-->Q) --> P)  -->  P)"
-  by rules
+  by iprover
 
 (* Problem 9 *)
 lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
-  by rules
+  by iprover
 
 (* Problem 10 *)
 lemma "(Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P=Q)"
-  by rules
+  by iprover
 
 (* 11.  Proved in each direction (incorrectly, says Pelletier!!) *)
 lemma "P=P"
-  by rules
+  by iprover
 
 (* Problem ~~12.  Dijkstra's law *)
 lemma "~~(((P = Q) = R)  =  (P = (Q = R)))"
-  by rules
+  by iprover
 
 lemma "((P = Q) = R)  -->  ~~(P = (Q = R))"
-  by rules
+  by iprover
 
 (* Problem 13.  Distributive law *)
 lemma "(P | (Q & R))  = ((P | Q) & (P | R))"
-  by rules
+  by iprover
 
 (* Problem ~~14 *)
 lemma "~~((P = Q) = ((Q | ~P) & (~Q|P)))"
-  by rules
+  by iprover
 
 (* Problem ~~15 *)
 lemma "~~((P --> Q) = (~P | Q))"
-  by rules
+  by iprover
 
 (* Problem ~~16 *)
 lemma "~~((P-->Q) | (Q-->P))"
-by rules
+by iprover
 
 (* Problem ~~17 *)
 lemma "~~(((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S)))"
@@ -171,7 +171,7 @@
 
 (*Dijkstra's "Golden Rule"*)
 lemma "(P&Q) = (P = (Q = (P|Q)))"
-  by rules
+  by iprover
 
 
 (****Examples with quantifiers****)
@@ -179,19 +179,19 @@
 (* The converse is classical in the following implications... *)
 
 lemma "(EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q"
-  by rules
+  by iprover
 
 lemma "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
-  by rules
+  by iprover
 
 lemma "((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))"
-  by rules
+  by iprover
 
 lemma "(ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)"
-  by rules 
+  by iprover 
 
 lemma "(EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
-  by rules
+  by iprover
 
 
 (* Hard examples with quantifiers *)
@@ -201,24 +201,24 @@
 
 (* Problem ~~19 *)
 lemma "~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))"
-  by rules
+  by iprover
 
 (* Problem 20 *)
 lemma "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
     --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
-  by rules
+  by iprover
 
 (* Problem 21 *)
 lemma "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P=Q(x))"
-  by rules
+  by iprover
 
 (* Problem 22 *)
 lemma "(ALL x. P = Q(x))  -->  (P = (ALL x. Q(x)))"
-  by rules
+  by iprover
 
 (* Problem ~~23 *)
 lemma "~~ ((ALL x. P | Q(x))  =  (P | (ALL x. Q(x))))"
-  by rules
+  by iprover
 
 (* Problem 25 *)
 lemma "(EX x. P(x)) &
@@ -226,7 +226,7 @@
        (ALL x. P(x) --> (M(x) & L(x))) &
        ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))
    --> (EX x. Q(x)&P(x))"
-  by rules
+  by iprover
 
 (* Problem 27 *)
 lemma "(EX x. P(x) & ~Q(x)) &
@@ -234,40 +234,40 @@
              (ALL x. M(x) & L(x) --> P(x)) &
              ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))
          --> (ALL x. M(x) --> ~L(x))"
-  by rules
+  by iprover
 
 (* Problem ~~28.  AMENDED *)
 lemma "(ALL x. P(x) --> (ALL x. Q(x))) &
        (~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &
        (~~(EX x. S(x)) --> (ALL x. L(x) --> M(x)))
    --> (ALL x. P(x) & L(x) --> M(x))"
-  by rules
+  by iprover
 
 (* Problem 29.  Essentially the same as Principia Mathematica *11.71 *)
 lemma "(((EX x. P(x)) & (EX y. Q(y))) -->
    (((ALL x. (P(x) --> R(x))) & (ALL y. (Q(y) --> S(y)))) =
     (ALL x y. ((P(x) & Q(y)) --> (R(x) & S(y))))))"
-  by rules
+  by iprover
 
 (* Problem ~~30 *)
 lemma "(ALL x. (P(x) | Q(x)) --> ~ R(x)) &
        (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
    --> (ALL x. ~~S(x))"
-  by rules
+  by iprover
 
 (* Problem 31 *)
 lemma "~(EX x. P(x) & (Q(x) | R(x))) & 
         (EX x. L(x) & P(x)) &
         (ALL x. ~ R(x) --> M(x))
     --> (EX x. L(x) & M(x))"
-  by rules
+  by iprover
 
 (* Problem 32 *)
 lemma "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
        (ALL x. S(x) & R(x) --> L(x)) &
        (ALL x. M(x) --> R(x))
    --> (ALL x. P(x) & M(x) --> L(x))"
-  by rules
+  by iprover
 
 (* Problem ~~33 *)
 lemma "(ALL x. ~~(P(a) & (P(x)-->P(b))-->P(c)))  =
@@ -280,50 +280,50 @@
       (ALL x. EX y. G x y) &
       (ALL x y. J x y | G x y --> (ALL z. J y z | G y z --> H x z))
   --> (ALL x. EX y. H x y)"
-  by rules
+  by iprover
 
 (* Problem 39 *)
 lemma "~ (EX x. ALL y. F y x = (~F y y))"
-  by rules
+  by iprover
 
 (* Problem 40.  AMENDED *)
 lemma "(EX y. ALL x. F x y = F x x) -->
              ~(ALL x. EX y. ALL z. F z y = (~ F z x))"
-  by rules
+  by iprover
 
 (* Problem 44 *)
 lemma "(ALL x. f(x) -->
              (EX y. g(y) & h x y & (EX y. g(y) & ~ h x y)))  &
              (EX x. j(x) & (ALL y. g(y) --> h x y))
              --> (EX x. j(x) & ~f(x))"
-  by rules
+  by iprover
 
 (* Problem 48 *)
 lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
-  by rules
+  by iprover
 
 (* Problem 51 *)
 lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) -->
   (EX z. (ALL x. (EX w. ((ALL y. (P x y = (y = w))) = (x = z))))))"
-  by rules
+  by iprover
 
 (* Problem 52 *)
 (*Almost the same as 51. *)
 lemma "((EX z w. (ALL x y. (P x y = ((x = z) & (y = w))))) -->
    (EX w. (ALL y. (EX z. ((ALL x. (P x y = (x = z))) = (y = w))))))"
-  by rules
+  by iprover
 
 (* Problem 56 *)
 lemma "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) = (ALL x. P(x) --> P(f(x)))"
-  by rules
+  by iprover
 
 (* Problem 57 *)
 lemma "P (f a b) (f b c) & P (f b c) (f a c) &
      (ALL x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)"
-  by rules
+  by iprover
 
 (* Problem 60 *)
 lemma "ALL x. P x (f x) = (EX y. (ALL z. P z y --> P z (f x)) & P x y)"
-  by rules
+  by iprover
 
 end