- Renamed inductive2 to inductive
- Renamed some theorems about transitive closure for predicates

--- a/src/HOL/Lambda/Commutation.thy	Wed Jul 11 11:22:02 2007 +0200
+++ b/src/HOL/Lambda/Commutation.thy	Wed Jul 11 11:23:24 2007 +0200
@@ -58,9 +58,9 @@
     "square R S S T ==> square (R^**) S S (T^**)"
   apply (unfold square_def)
   apply (intro strip)
-  apply (erule rtrancl_induct')
+  apply (erule rtranclp_induct)
    apply blast
-  apply (blast intro: rtrancl.rtrancl_into_rtrancl)
+  apply (blast intro: rtranclp.rtrancl_into_rtrancl)
   done
 
 lemma square_rtrancl_reflcl_commute:
@@ -110,14 +110,14 @@
 
 lemma confluent_Un:
     "[| confluent R; confluent S; commute (R^**) (S^**) |] ==> confluent (sup R S)"
-  apply (rule rtrancl_Un_rtrancl' [THEN subst])
+  apply (rule rtranclp_sup_rtranclp [THEN subst])
   apply (blast dest: diamond_Un intro: diamond_confluent)
   done
 
 lemma diamond_to_confluence:
     "[| diamond R; T \<le> R; R \<le> T^** |] ==> confluent T"
   apply (force intro: diamond_confluent
-    dest: rtrancl_subset' [symmetric])
+    dest: rtranclp_subset [symmetric])
   done
 
 
@@ -128,12 +128,12 @@
   apply (tactic {* safe_tac HOL_cs *})
    apply (tactic {*
      blast_tac (HOL_cs addIs
-       [thm "sup_ge2" RS thm "rtrancl_mono'" RS thm "predicate2D" RS thm "rtrancl_trans'",
-        thm "rtrancl_converseI'", thm "conversepI",
-        thm "sup_ge1" RS thm "rtrancl_mono'" RS thm "predicate2D"]) 1 *})
-  apply (erule rtrancl_induct')
+       [thm "sup_ge2" RS thm "rtranclp_mono" RS thm "predicate2D" RS thm "rtranclp_trans",
+        thm "rtranclp_converseI", thm "conversepI",
+        thm "sup_ge1" RS thm "rtranclp_mono" RS thm "predicate2D"]) 1 *})
+  apply (erule rtranclp_induct)
    apply blast
-  apply (blast del: rtrancl.rtrancl_refl intro: rtrancl_trans')
+  apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_trans)
   done
 
 
@@ -152,7 +152,7 @@
   case (less x b c)
   have xc: "R\<^sup>*\<^sup>* x c" by fact
   have xb: "R\<^sup>*\<^sup>* x b" by fact thus ?case
-  proof (rule converse_rtranclE')
+  proof (rule converse_rtranclpE)
     assume "x = b"
     with xc have "R\<^sup>*\<^sup>* b c" by simp
     thus ?thesis by iprover
@@ -161,7 +161,7 @@
     assume xy: "R x y"
     assume yb: "R\<^sup>*\<^sup>* y b"
     from xc show ?thesis
-    proof (rule converse_rtranclE')
+    proof (rule converse_rtranclpE)
       assume "x = c"
       with xb have "R\<^sup>*\<^sup>* c b" by simp
       thus ?thesis by iprover
@@ -175,11 +175,11 @@
       from this and yb yu have "\<exists>d. R\<^sup>*\<^sup>* b d \<and> R\<^sup>*\<^sup>* u d" by (rule less)
       then obtain v where bv: "R\<^sup>*\<^sup>* b v" and uv: "R\<^sup>*\<^sup>* u v" by iprover
       from xy' have "R\<inverse>\<inverse> y' x" ..
-      moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtrancl_trans')
+      moreover from y'u and uv have "R\<^sup>*\<^sup>* y' v" by (rule rtranclp_trans)
       moreover note y'c
       ultimately have "\<exists>d. R\<^sup>*\<^sup>* v d \<and> R\<^sup>*\<^sup>* c d" by (rule less)
       then obtain w where vw: "R\<^sup>*\<^sup>* v w" and cw: "R\<^sup>*\<^sup>* c w" by iprover
-      from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtrancl_trans')
+      from bv vw have "R\<^sup>*\<^sup>* b w" by (rule rtranclp_trans)
       with cw show ?thesis by iprover
     qed
   qed
@@ -206,7 +206,7 @@
   have xc: "R\<^sup>*\<^sup>* x c" by fact
   have xb: "R\<^sup>*\<^sup>* x b" by fact
   thus ?case
-  proof (rule converse_rtranclE')
+  proof (rule converse_rtranclpE)
     assume "x = b"
     with xc have "R\<^sup>*\<^sup>* b c" by simp
     thus ?thesis by iprover
@@ -215,7 +215,7 @@
     assume xy: "R x y"
     assume yb: "R\<^sup>*\<^sup>* y b"
     from xc show ?thesis
-    proof (rule converse_rtranclE')
+    proof (rule converse_rtranclpE)
       assume "x = c"
       with xb have "R\<^sup>*\<^sup>* c b" by simp
       thus ?thesis by iprover
@@ -226,8 +226,8 @@
       with xy obtain u where u: "R\<^sup>*\<^sup>* y u" "R\<^sup>*\<^sup>* y' u"
         by (blast dest: lc)
       from yb u y'c show ?thesis
-        by (blast del: rtrancl.rtrancl_refl
-            intro: rtrancl_trans'
+        by (blast del: rtranclp.rtrancl_refl
+            intro: rtranclp_trans
             dest: IH [OF conversepI, OF xy] IH [OF conversepI, OF xy'])
     qed
   qed

--- a/src/HOL/Lambda/Eta.thy	Wed Jul 11 11:22:02 2007 +0200
+++ b/src/HOL/Lambda/Eta.thy	Wed Jul 11 11:23:24 2007 +0200
@@ -18,7 +18,7 @@
   "free (s \<degree> t) i = (free s i \<or> free t i)"
   "free (Abs s) i = free s (i + 1)"
 
-inductive2 eta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<eta>" 50)
+inductive eta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<eta>" 50)
   where
     eta [simp, intro]: "\<not> free s 0 ==> Abs (s \<degree> Var 0) \<rightarrow>\<^sub>\<eta> s[dummy/0]"
   | appL [simp, intro]: "s \<rightarrow>\<^sub>\<eta> t ==> s \<degree> u \<rightarrow>\<^sub>\<eta> t \<degree> u"
@@ -37,7 +37,7 @@
   eta_reds  (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>*" 50) and
   eta_red0  (infixl "\<rightarrow>\<^sub>\<eta>\<^sup>=" 50)
 
-inductive_cases2 eta_cases [elim!]:
+inductive_cases eta_cases [elim!]:
   "Abs s \<rightarrow>\<^sub>\<eta> z"
   "s \<degree> t \<rightarrow>\<^sub>\<eta> u"
   "Var i \<rightarrow>\<^sub>\<eta> t"
@@ -103,19 +103,19 @@
 subsection "Congruence rules for eta*"
 
 lemma rtrancl_eta_Abs: "s \<rightarrow>\<^sub>\<eta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<eta>\<^sup>* Abs s'"
-  by (induct set: rtrancl)
-    (blast intro: rtrancl.rtrancl_into_rtrancl)+
+  by (induct set: rtranclp)
+    (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma rtrancl_eta_AppL: "s \<rightarrow>\<^sub>\<eta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s' \<degree> t"
-  by (induct set: rtrancl)
-    (blast intro: rtrancl.rtrancl_into_rtrancl)+
+  by (induct set: rtranclp)
+    (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma rtrancl_eta_AppR: "t \<rightarrow>\<^sub>\<eta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s \<degree> t'"
-  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma rtrancl_eta_App:
     "[| s \<rightarrow>\<^sub>\<eta>\<^sup>* s'; t \<rightarrow>\<^sub>\<eta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<eta>\<^sup>* s' \<degree> t'"
-  by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans')
+  by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtranclp_trans)
 
 
 subsection "Commutation of beta and eta"
@@ -149,7 +149,7 @@
 lemma rtrancl_eta_subst'':
   assumes eta: "s \<rightarrow>\<^sub>\<eta>\<^sup>* t"
   shows "u[s/i] \<rightarrow>\<^sub>\<eta>\<^sup>* u[t/i]" using eta
-  by induct (iprover intro: rtrancl_eta_subst rtrancl_trans')+
+  by induct (iprover intro: rtrancl_eta_subst rtranclp_trans)+
 
 lemma square_beta_eta: "square beta eta (eta^**) (beta^==)"
   apply (unfold square_def)
@@ -361,7 +361,7 @@
     by (auto dest: eta_par_beta)
   from s' obtain t'' where s: "s => t''" and t'': "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* t'" using 2
     by blast
-  from t'' and t' have "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* s'''" by (rule rtrancl_trans')
+  from t'' and t' have "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* s'''" by (rule rtranclp_trans)
   with s show ?case by iprover
 qed
 
@@ -381,7 +381,7 @@
     with t' obtain t'' where st: "t' => t''" and tu: "t'' \<rightarrow>\<^sub>\<eta>\<^sup>* s''"
       by (auto dest: eta_postponement')
     from par_beta_subset_beta st have "t' \<rightarrow>\<^sub>\<beta>\<^sup>* t''" ..
-    with s have "s \<rightarrow>\<^sub>\<beta>\<^sup>* t''" by (rule rtrancl_trans')
+    with s have "s \<rightarrow>\<^sub>\<beta>\<^sup>* t''" by (rule rtranclp_trans)
     thus ?thesis using tu ..
   next
     assume "s' \<rightarrow>\<^sub>\<eta> s''"

--- a/src/HOL/Lambda/InductTermi.thy	Wed Jul 11 11:22:02 2007 +0200
+++ b/src/HOL/Lambda/InductTermi.thy	Wed Jul 11 11:23:24 2007 +0200
@@ -14,7 +14,7 @@
 
 subsection {* Terminating lambda terms *}
 
-inductive2 IT :: "dB => bool"
+inductive IT :: "dB => bool"
   where
     Var [intro]: "listsp IT rs ==> IT (Var n \<degree>\<degree> rs)"
   | Lambda [intro]: "IT r ==> IT (Abs r)"
@@ -24,33 +24,33 @@
 subsection {* Every term in IT terminates *}
 
 lemma double_induction_lemma [rule_format]:
-  "termi beta s ==> \<forall>t. termi beta t -->
-    (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termi beta (Abs r \<degree> s \<degree>\<degree> ss))"
-  apply (erule acc_induct)
+  "termip beta s ==> \<forall>t. termip beta t -->
+    (\<forall>r ss. t = r[s/0] \<degree>\<degree> ss --> termip beta (Abs r \<degree> s \<degree>\<degree> ss))"
+  apply (erule accp_induct)
   apply (rule allI)
   apply (rule impI)
   apply (erule thin_rl)
-  apply (erule acc_induct)
+  apply (erule accp_induct)
   apply clarify
-  apply (rule accI)
+  apply (rule accp.accI)
   apply (safe elim!: apps_betasE)
      apply assumption
     apply (blast intro: subst_preserves_beta apps_preserves_beta)
-   apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI'
-     dest: acc_downwards)  (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
+   apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtranclp_converseI
+     dest: accp_downwards)  (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
   apply (blast dest: apps_preserves_betas)
   done
 
-lemma IT_implies_termi: "IT t ==> termi beta t"
+lemma IT_implies_termi: "IT t ==> termip beta t"
   apply (induct set: IT)
-    apply (drule rev_predicate1D [OF _ listsp_mono [where B="termi beta"]])
+    apply (drule rev_predicate1D [OF _ listsp_mono [where B="termip beta"]])
     apply fast
     apply (drule lists_accD)
-    apply (erule acc_induct)
-    apply (rule accI)
+    apply (erule accp_induct)
+    apply (rule accp.accI)
     apply (blast dest: head_Var_reduction)
-   apply (erule acc_induct)
-   apply (rule accI)
+   apply (erule accp_induct)
+   apply (rule accp.accI)
    apply blast
   apply (blast intro: double_induction_lemma)
   done
@@ -67,13 +67,13 @@
   "(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')"
   by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
 
-inductive_cases2 [elim!]:
+inductive_cases [elim!]:
   "IT (Var n \<degree>\<degree> ss)"
   "IT (Abs t)"
   "IT (Abs r \<degree> s \<degree>\<degree> ts)"
 
-theorem termi_implies_IT: "termi beta r ==> IT r"
-  apply (erule acc_induct)
+theorem termi_implies_IT: "termip beta r ==> IT r"
+  apply (erule accp_induct)
   apply (rename_tac r)
   apply (erule thin_rl)
   apply (erule rev_mp)

--- a/src/HOL/Lambda/Lambda.thy	Wed Jul 11 11:22:02 2007 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Wed Jul 11 11:23:24 2007 +0200
@@ -53,7 +53,7 @@
 
 subsection {* Beta-reduction *}
 
-inductive2 beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
   where
     beta [simp, intro!]: "Abs s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
   | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
@@ -67,7 +67,7 @@
 notation (latex)
   beta_reds  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
 
-inductive_cases2 beta_cases [elim!]:
+inductive_cases beta_cases [elim!]:
   "Var i \<rightarrow>\<^sub>\<beta> t"
   "Abs r \<rightarrow>\<^sub>\<beta> s"
   "s \<degree> t \<rightarrow>\<^sub>\<beta> u"
@@ -80,19 +80,19 @@
 
 lemma rtrancl_beta_Abs [intro!]:
     "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
-  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_AppL:
     "s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
-  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_AppR:
     "t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
-  by (induct set: rtrancl) (blast intro: rtrancl.rtrancl_into_rtrancl)+
+  by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+
 
 lemma rtrancl_beta_App [intro]:
     "[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
-  by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtrancl_trans')
+  by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans)
 
 
 subsection {* Substitution-lemmas *}
@@ -155,9 +155,9 @@
   by (induct arbitrary: t i set: beta) (simp_all add: subst_subst [symmetric])
 
 theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
-  apply (induct set: rtrancl)
-   apply (rule rtrancl.rtrancl_refl)
-  apply (erule rtrancl.rtrancl_into_rtrancl)
+  apply (induct set: rtranclp)
+   apply (rule rtranclp.rtrancl_refl)
+  apply (erule rtranclp.rtrancl_into_rtrancl)
   apply (erule subst_preserves_beta)
   done
 
@@ -166,23 +166,23 @@
   by (induct arbitrary: i set: beta) auto
 
 theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
-  apply (induct set: rtrancl)
-   apply (rule rtrancl.rtrancl_refl)
-  apply (erule rtrancl.rtrancl_into_rtrancl)
+  apply (induct set: rtranclp)
+   apply (rule rtranclp.rtrancl_refl)
+  apply (erule rtranclp.rtrancl_into_rtrancl)
   apply (erule lift_preserves_beta)
   done
 
 theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
   apply (induct t arbitrary: r s i)
-    apply (simp add: subst_Var r_into_rtrancl')
+    apply (simp add: subst_Var r_into_rtranclp)
    apply (simp add: rtrancl_beta_App)
   apply (simp add: rtrancl_beta_Abs)
   done
 
 theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
-  apply (induct set: rtrancl)
-   apply (rule rtrancl.rtrancl_refl)
-  apply (erule rtrancl_trans')
+  apply (induct set: rtranclp)
+   apply (rule rtranclp.rtrancl_refl)
+  apply (erule rtranclp_trans)
   apply (erule subst_preserves_beta2)
   done
 

--- a/src/HOL/Lambda/ListBeta.thy	Wed Jul 11 11:22:02 2007 +0200
+++ b/src/HOL/Lambda/ListBeta.thy	Wed Jul 11 11:23:24 2007 +0200
@@ -71,9 +71,9 @@
 
 lemma apps_preserves_beta2 [simp]:
     "r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
-  apply (induct set: rtrancl)
+  apply (induct set: rtranclp)
    apply blast
-  apply (blast intro: apps_preserves_beta rtrancl.rtrancl_into_rtrancl)
+  apply (blast intro: apps_preserves_beta rtranclp.rtrancl_into_rtrancl)
   done
 
 lemma apps_preserves_betas [simp]:

--- a/src/HOL/Lambda/ListOrder.thy	Wed Jul 11 11:22:02 2007 +0200
+++ b/src/HOL/Lambda/ListOrder.thy	Wed Jul 11 11:23:24 2007 +0200
@@ -87,20 +87,20 @@
   done
 
 lemma Cons_acc_step1I [intro!]:
-    "acc r x ==> acc (step1 r) xs \<Longrightarrow> acc (step1 r) (x # xs)"
-  apply (induct arbitrary: xs set: acc)
+    "accp r x ==> accp (step1 r) xs \<Longrightarrow> accp (step1 r) (x # xs)"
+  apply (induct arbitrary: xs set: accp)
   apply (erule thin_rl)
-  apply (erule acc_induct)
-  apply (rule accI)
+  apply (erule accp_induct)
+  apply (rule accp.accI)
   apply blast
   done
 
-lemma lists_accD: "listsp (acc r) xs ==> acc (step1 r) xs"
+lemma lists_accD: "listsp (accp r) xs ==> accp (step1 r) xs"
   apply (induct set: listsp)
-   apply (rule accI)
+   apply (rule accp.accI)
    apply simp
-  apply (rule accI)
-  apply (fast dest: acc_downward)
+  apply (rule accp.accI)
+  apply (fast dest: accp_downward)
   done
 
 lemma ex_step1I:
@@ -111,10 +111,10 @@
   apply force
   done
 
-lemma lists_accI: "acc (step1 r) xs ==> listsp (acc r) xs"
-  apply (induct set: acc)
+lemma lists_accI: "accp (step1 r) xs ==> listsp (accp r) xs"
+  apply (induct set: accp)
   apply clarify
-  apply (rule accI)
+  apply (rule accp.accI)
   apply (drule_tac r=r in ex_step1I, assumption)
   apply blast
   done

--- a/src/HOL/Lambda/ParRed.thy	Wed Jul 11 11:22:02 2007 +0200
+++ b/src/HOL/Lambda/ParRed.thy	Wed Jul 11 11:23:24 2007 +0200
@@ -14,14 +14,14 @@
 
 subsection {* Parallel reduction *}
 
-inductive2 par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
+inductive par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
   where
     var [simp, intro!]: "Var n => Var n"
   | abs [simp, intro!]: "s => t ==> Abs s => Abs t"
   | app [simp, intro!]: "[| s => s'; t => t' |] ==> s \<degree> t => s' \<degree> t'"
   | beta [simp, intro!]: "[| s => s'; t => t' |] ==> (Abs s) \<degree> t => s'[t'/0]"
 
-inductive_cases2 par_beta_cases [elim!]:
+inductive_cases par_beta_cases [elim!]:
   "Var n => t"
   "Abs s => Abs t"
   "(Abs s) \<degree> t => u"
@@ -50,7 +50,7 @@
   apply (rule predicate2I)
   apply (erule par_beta.induct)
      apply blast
-    apply (blast del: rtrancl.rtrancl_refl intro: rtrancl.rtrancl_into_rtrancl)+
+    apply (blast del: rtranclp.rtrancl_refl intro: rtranclp.rtrancl_into_rtrancl)+
       -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
   done
 

--- a/src/HOL/Lambda/StrongNorm.thy	Wed Jul 11 11:22:02 2007 +0200
+++ b/src/HOL/Lambda/StrongNorm.thy	Wed Jul 11 11:23:24 2007 +0200
@@ -277,7 +277,7 @@
   thus ?case by simp
 qed
 
-theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> termi beta t"
+theorem type_implies_termi: "e \<turnstile> t : T \<Longrightarrow> termip beta t"
 proof -
   assume "e \<turnstile> t : T"
   hence "IT t" by (rule type_implies_IT)

--- a/src/HOL/Lambda/Type.thy	Wed Jul 11 11:22:02 2007 +0200
+++ b/src/HOL/Lambda/Type.thy	Wed Jul 11 11:23:24 2007 +0200
@@ -45,13 +45,13 @@
     Atom nat
   | Fun type type    (infixr "\<Rightarrow>" 200)
 
-inductive2 typing :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
+inductive typing :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
   where
     Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T"
   | Abs [intro!]: "env\<langle>0:T\<rangle> \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs t : (T \<Rightarrow> U)"
   | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
 
-inductive_cases2 typing_elims [elim!]:
+inductive_cases typing_elims [elim!]:
   "e \<turnstile> Var i : T"
   "e \<turnstile> t \<degree> u : T"
   "e \<turnstile> Abs t : T"
@@ -164,7 +164,7 @@
   apply (erule impE)
    apply assumption
   apply (elim exE conjE)
-  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
+  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
   apply (rule_tac x = "Ta # Ts" in exI)
   apply simp
   done
@@ -202,12 +202,12 @@
   "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
   apply (induct ts arbitrary: T U rule: rev_induct)
   apply simp
-  apply (ind_cases2 "e \<turnstile> Var i : T" for T)
-  apply (ind_cases2 "e \<turnstile> Var i : T" for T)
+  apply (ind_cases "e \<turnstile> Var i : T" for T)
+  apply (ind_cases "e \<turnstile> Var i : T" for T)
   apply simp
   apply simp
-  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
-  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
+  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
+  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
   apply atomize
   apply (erule_tac x="Ta \<Rightarrow> T" in allE)
   apply (erule_tac x="Tb \<Rightarrow> U" in allE)
@@ -230,7 +230,7 @@
   apply (rule FalseE)
   apply simp
   apply (erule list_app_typeE)
-  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
+  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
   apply (drule_tac T="Atom nat" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
   apply assumption
   apply simp
@@ -242,7 +242,7 @@
   apply (rule types_snoc)
   apply assumption
   apply (erule list_app_typeE)
-  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
+  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
   apply (drule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
   apply assumption
   apply simp
@@ -250,7 +250,7 @@
   apply (rule typing.App)
   apply assumption
   apply (erule list_app_typeE)
-  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
+  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
   apply (frule_tac T="type1 \<Rightarrow> type2" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
   apply assumption
   apply simp
@@ -258,7 +258,7 @@
   apply (rule_tac x="type1 # Us" in exI)
   apply simp
   apply (erule list_app_typeE)
-  apply (ind_cases2 "e \<turnstile> t \<degree> u : T" for t u T)
+  apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
   apply (frule_tac T="type1 \<Rightarrow> Us \<Rrightarrow> T" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
   apply assumption
   apply simp
@@ -332,9 +332,9 @@
     apply blast
    apply blast
   apply atomize
-  apply (ind_cases2 "s \<degree> t \<rightarrow>\<^sub>\<beta> t'" for s t t')
+  apply (ind_cases "s \<degree> t \<rightarrow>\<^sub>\<beta> t'" for s t t')
     apply hypsubst
-    apply (ind_cases2 "env \<turnstile> Abs t : T \<Rightarrow> U" for env t T U)
+    apply (ind_cases "env \<turnstile> Abs t : T \<Rightarrow> U" for env t T U)
     apply (rule subst_lemma)
       apply assumption
      apply assumption
@@ -344,7 +344,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) (iprover intro: subject_reduction)+
+  by (induct set: rtranclp) (iprover intro: subject_reduction)+
 
 
 subsection {* Alternative induction rule for types *}

--- a/src/HOL/Lambda/WeakNorm.thy	Wed Jul 11 11:22:02 2007 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Wed Jul 11 11:23:24 2007 +0200
@@ -75,7 +75,7 @@
   -- {* Currently needed for strange technical reasons *}
   by (unfold listall_def) simp
 
-inductive2 NF :: "dB \<Rightarrow> bool"
+inductive NF :: "dB \<Rightarrow> bool"
 where
   App: "listall NF ts \<Longrightarrow> NF (Var x \<degree>\<degree> ts)"
 | Abs: "NF t \<Longrightarrow> NF (Abs t)"
@@ -138,15 +138,15 @@
   apply (simplesubst app_last)  --{*Using @{text subst} makes extraction fail*}
   apply (rule exI)
   apply (rule conjI)
-  apply (rule rtrancl.rtrancl_refl)
+  apply (rule rtranclp.rtrancl_refl)
   apply (rule NF.App)
   apply (drule listall_conj1)
   apply (simp add: listall_app)
   apply (rule Var_NF)
   apply (rule exI)
   apply (rule conjI)
-  apply (rule rtrancl.rtrancl_into_rtrancl)
-  apply (rule rtrancl.rtrancl_refl)
+  apply (rule rtranclp.rtrancl_into_rtrancl)
+  apply (rule rtranclp.rtrancl_refl)
   apply (rule beta)
   apply (erule subst_Var_NF)
   done
@@ -361,7 +361,7 @@
 
 
 -- {* A computationally relevant copy of @{term "e \<turnstile> t : T"} *}
-inductive2 rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
+inductive rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
   where
     Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T"
   | Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"
@@ -411,7 +411,7 @@
   qed
   then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "NF u" 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')
+  hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtranclp_trans)
   with unf show ?case by iprover
 qed
 
@@ -419,21 +419,21 @@
 subsection {* Extracting the program *}
 
 declare NF.induct [ind_realizer]
-declare rtrancl.induct [ind_realizer irrelevant]
+declare rtranclp.induct [ind_realizer irrelevant]
 declare rtyping.induct [ind_realizer]
 lemmas [extraction_expand] = conj_assoc listall_cons_eq
 
 extract type_NF
 
-lemma rtranclR_rtrancl_eq: "rtranclR r a b = rtrancl r a b"
+lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
   apply (rule iffI)
-  apply (erule rtranclR.induct)
-  apply (rule rtrancl.rtrancl_refl)
-  apply (erule rtrancl.rtrancl_into_rtrancl)
+  apply (erule rtranclpR.induct)
+  apply (rule rtranclp.rtrancl_refl)
+  apply (erule rtranclp.rtrancl_into_rtrancl)
   apply assumption
-  apply (erule rtrancl.induct)
-  apply (rule rtranclR.rtrancl_refl)
-  apply (erule rtranclR.rtrancl_into_rtrancl)
+  apply (erule rtranclp.induct)
+  apply (rule rtranclpR.rtrancl_refl)
+  apply (erule rtranclpR.rtrancl_into_rtrancl)
   apply assumption
   done