# HG changeset patch
# User berghofe
# Date 1184146566 -7200
# Node ID aca2c7f80e2fbcea34e41c629cb10c44c92a9e80
# Parent  90bccef650049c1c4be39588a0d1969fc206032e
Renamed inductive2 to inductive.

diff -r 90bccef65004 -r aca2c7f80e2f src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Wed Jul 11 11:35:17 2007 +0200
+++ b/src/HOL/Nominal/Examples/CR.thy	Wed Jul 11 11:36:06 2007 +0200
@@ -147,7 +147,7 @@
 
 section {* Beta Reduction *}
 
-inductive2
+inductive
   "Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
 where
     b1[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
@@ -160,7 +160,7 @@
 nominal_inductive Beta
   by (simp_all add: abs_fresh fresh_fact')
 
-inductive2
+inductive
   "Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
 where
     bs1[intro, simp]: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
@@ -177,7 +177,7 @@
 
 section {* One-Reduction *}
 
-inductive2
+inductive
   One :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1 _" [80,80] 80)
 where
     o1[intro!]:      "M\<longrightarrow>\<^isub>1M"
@@ -190,7 +190,7 @@
 nominal_inductive One
   by (simp_all add: abs_fresh fresh_fact')
 
-inductive2
+inductive
   "One_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80)
 where
     os1[intro, simp]: "M \<longrightarrow>\<^isub>1\<^sup>* M"
@@ -272,7 +272,7 @@
   shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''"
   using a
   apply -
-  apply(ind_cases2 "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
+  apply(ind_cases "(Lam [a].t)\<longrightarrow>\<^isub>1t'")
   apply(auto simp add: lam.inject alpha)
   apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
   apply(rule conjI)
@@ -289,7 +289,7 @@
          (\<exists>a s s1 s2. t1 = Lam [a].s \<and> a\<sharp>(t2,s2) \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
   using a
   apply -
-  apply(ind_cases2 "App t1 t2 \<longrightarrow>\<^isub>1 t'")
+  apply(ind_cases "App t1 t2 \<longrightarrow>\<^isub>1 t'")
   apply(auto simp add: lam.distinct lam.inject)
   done
 
@@ -299,7 +299,7 @@
          (\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
   using a
   apply -
-  apply(ind_cases2 "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M")
+  apply(ind_cases "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M")
   apply(simp_all add: lam.inject)
   apply(force)
   apply(erule conjE)
diff -r 90bccef65004 -r aca2c7f80e2f src/HOL/Nominal/Examples/CR_Takahashi.thy
--- a/src/HOL/Nominal/Examples/CR_Takahashi.thy	Wed Jul 11 11:35:17 2007 +0200
+++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy	Wed Jul 11 11:36:06 2007 +0200
@@ -71,7 +71,7 @@
 
 section {* Beta-Reduction *}
 
-inductive2 
+inductive 
   "Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
 where
   b1[intro]: "t1 \<longrightarrow>\<^isub>\<beta> t2 \<Longrightarrow> App t1 s \<longrightarrow>\<^isub>\<beta> App t2 s"
@@ -81,7 +81,7 @@
 
 section {* Transitive Closure of Beta *}
 
-inductive2 
+inductive 
   "Beta_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
 where
   bs1[intro]: "t \<longrightarrow>\<^isub>\<beta>\<^sup>* t"
@@ -90,7 +90,7 @@
 
 section {* One-Reduction *}
 
-inductive2 
+inductive 
   One :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1 _" [80,80] 80)
 where
   o1[intro]: "Var x\<longrightarrow>\<^isub>1 Var x"
@@ -169,7 +169,7 @@
 
 section {* Transitive Closure of One *}
 
-inductive2 
+inductive 
   "One_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80)
 where
   os1[intro]: "t \<longrightarrow>\<^isub>1\<^sup>* t"
@@ -178,7 +178,7 @@
 
 section {* Complete Development Reduction *}
 
-inductive2 
+inductive 
   Dev :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>d _" [80,80]80)
 where
   d1[intro]: "Var x \<longrightarrow>\<^isub>d Var x"
diff -r 90bccef65004 -r aca2c7f80e2f src/HOL/Nominal/Examples/Compile.thy
--- a/src/HOL/Nominal/Examples/Compile.thy	Wed Jul 11 11:35:17 2007 +0200
+++ b/src/HOL/Nominal/Examples/Compile.thy	Wed Jul 11 11:36:06 2007 +0200
@@ -50,7 +50,7 @@
 
 text {* valid contexts *}
 
-inductive2 
+inductive 
   valid :: "(name\<times>'a::pt_name) list \<Rightarrow> bool"
 where
   v1[intro]: "valid []"
@@ -58,7 +58,7 @@
 
 text {* typing judgements for trms *}
 
-inductive2 
+inductive 
   typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)
 where
   t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : \<tau>"
@@ -76,7 +76,7 @@
 
 text {* typing judgements for Itrms *}
 
-inductive2 
+inductive 
   Ityping :: "(name\<times>tyI) list\<Rightarrow>trmI\<Rightarrow>tyI\<Rightarrow>bool" (" _ I\<turnstile> _ : _ " [80,80,80] 80)
 where
   t0[intro]: "\<lbrakk>valid \<Gamma>; (x,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> I\<turnstile> IVar x : \<tau>"
@@ -167,7 +167,7 @@
 
 text {* big-step evaluation for trms *}
 
-inductive2 
+inductive 
   big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80)
 where
   b0[intro]: "Lam [x].e \<Down> Lam [x].e"
@@ -181,7 +181,7 @@
 | b8[intro]: "\<lbrakk>e\<Down>InL e'; e1[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
 | b9[intro]: "\<lbrakk>e\<Down>InR e'; e2[x::=e']\<Down>e''\<rbrakk> \<Longrightarrow> Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2 \<Down> e''"
 
-inductive2 
+inductive 
   Ibig :: "((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>((nat\<Rightarrow>nat)\<times>trmI)\<Rightarrow>bool" ("_ I\<Down> _" [80,80] 80)
 where
   m0[intro]: "(m,ILam [x].e) I\<Down> (m,ILam [x].e)"
diff -r 90bccef65004 -r aca2c7f80e2f src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Wed Jul 11 11:35:17 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Wed Jul 11 11:36:06 2007 +0200
@@ -257,7 +257,7 @@
 
 section {* Typing *}
 
-inductive2
+inductive
   valid :: "Ctxt \<Rightarrow> bool"
 where
   v_nil[intro]:  "valid []"
@@ -265,7 +265,7 @@
 
 equivariance valid 
 
-inductive_cases2  
+inductive_cases  
   valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)"
 
 abbreviation
@@ -297,7 +297,7 @@
 by (induct \<Gamma>)
    (auto dest!: fresh_context)
 
-inductive2
+inductive
   typing :: "Ctxt\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) 
 where
   t_Var[intro]:   "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
@@ -319,7 +319,7 @@
 declare trm.inject [simp add]
 declare ty.inject  [simp add]
 
-inductive_cases2 t_inv_auto[elim]: 
+inductive_cases t_inv_auto[elim]: 
   "\<Gamma> \<turnstile> Lam [x].t : T"
   "\<Gamma> \<turnstile> Var x : T"
   "\<Gamma> \<turnstile> App x y : T"
@@ -332,7 +332,7 @@
 
 section {* Definitional Equivalence *}
 
-inductive2
+inductive
   def_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<equiv> _ : _" [60,60] 60) 
 where
   Q_Refl[intro]:  "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<equiv> t : T"
@@ -358,7 +358,7 @@
 
 section {* Weak Head Reduction *}
 
-inductive2
+inductive
   whr_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<leadsto> _" [80,80] 80) 
 where
   QAR_Beta[intro]: "App (Lam [x]. t\<^isub>1) t\<^isub>2 \<leadsto> t\<^isub>1[x::=t\<^isub>2]"
@@ -367,7 +367,7 @@
 declare trm.inject  [simp add]
 declare ty.inject  [simp add]
 
-inductive_cases2 whr_inv_auto[elim]: 
+inductive_cases whr_inv_auto[elim]: 
   "t \<leadsto> t'"
   "Lam [x].t \<leadsto> t'"
   "App (Lam [x].t12) t2 \<leadsto> t"
@@ -390,7 +390,7 @@
 where
   "t\<leadsto>|  \<equiv> \<not>(\<exists> u. t \<leadsto> u)" 
 
-inductive2
+inductive
   whn_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) 
 where
   QAN_Reduce[intro]: "\<lbrakk>s \<leadsto> t; t \<Down> u\<rbrakk> \<Longrightarrow> s \<Down> u"
@@ -398,7 +398,7 @@
 
 declare trm.inject[simp]
 
-inductive_cases2 whn_inv_auto[elim]: "t \<Down> t'"
+inductive_cases whn_inv_auto[elim]: "t \<Down> t'"
 
 declare trm.inject[simp del]
 
@@ -448,7 +448,7 @@
 
 section {* Algorithmic Term Equivalence and Algorithmic Path Equivalence *}
 
-inductive2
+inductive
   alg_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<Leftrightarrow> _ : _" [60,60,60,60] 60) 
 and
   alg_path_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<leftrightarrow> _ : _" [60,60,60,60] 60) 
@@ -470,11 +470,11 @@
 declare trm.inject [simp add]
 declare ty.inject  [simp add]
 
-inductive_cases2 alg_equiv_inv_auto[elim]: 
+inductive_cases alg_equiv_inv_auto[elim]: 
   "\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase"
   "\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
 
-inductive_cases2 alg_path_equiv_inv_auto[elim]: 
+inductive_cases alg_path_equiv_inv_auto[elim]: 
   "\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase"
   "\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit"
   "\<Gamma> \<turnstile> s\<leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
diff -r 90bccef65004 -r aca2c7f80e2f src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Wed Jul 11 11:35:17 2007 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Wed Jul 11 11:36:06 2007 +0200
@@ -177,7 +177,7 @@
 
 text {* Now validity of a context is a straightforward inductive definition. *}
   
-inductive2 
+inductive 
   valid_rel :: "ty_context \<Rightarrow> bool" ("\<turnstile> _ ok" [100] 100)
 where
   valid_nil[simp]:  "\<turnstile> [] ok"
@@ -279,7 +279,7 @@
   does \emph{not} make the subtyping-relation ``partial"\ldots because we work over
   $\alpha$-equivalence classes.) *}
 
-inductive2 
+inductive 
   subtype_of :: "ty_context \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"   ("_\<turnstile>_<:_" [100,100,100] 100)
 where
   S_Top[intro]:    "\<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
@@ -509,7 +509,7 @@
   shows "\<lbrakk>\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T; X\<sharp>\<Gamma>; X\<sharp>S\<^isub>1\<rbrakk>
          \<Longrightarrow> T = Top \<or> (\<exists>T\<^isub>1 T\<^isub>2. T = \<forall>[X<:T\<^isub>1].T\<^isub>2 \<and> \<Gamma> \<turnstile> T\<^isub>1 <: S\<^isub>1 \<and> ((X,T\<^isub>1)#\<Gamma>) \<turnstile> S\<^isub>2 <: T\<^isub>2)"
   apply(frule subtype_implies_ok)
-  apply(ind_cases2 "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T")
+  apply(ind_cases "\<Gamma> \<turnstile> \<forall>[X<:S\<^isub>1].S\<^isub>2 <: T")
   apply(auto simp add: ty.inject alpha)
   apply(rule_tac x="[(X,Xa)]\<bullet>T\<^isub>2" in exI)
   apply(rule conjI)
diff -r 90bccef65004 -r aca2c7f80e2f src/HOL/Nominal/Examples/LocalWeakening.thy
--- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Wed Jul 11 11:35:17 2007 +0200
+++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Wed Jul 11 11:36:06 2007 +0200
@@ -96,7 +96,7 @@
 
 types cxt = "(name\<times>ty) list"
 
-inductive2
+inductive
   valid :: "cxt \<Rightarrow> bool"
 where
   v1[intro]: "valid []"
@@ -112,7 +112,7 @@
 
 text {* "weak" typing relation *}
 
-inductive2
+inductive
   typing :: "cxt\<Rightarrow>llam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60)
 where
     t_lPar[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> lPar x : T"
diff -r 90bccef65004 -r aca2c7f80e2f src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Wed Jul 11 11:35:17 2007 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy	Wed Jul 11 11:36:06 2007 +0200
@@ -59,7 +59,7 @@
 by (nominal_induct t avoiding: \<theta> c s rule: lam.induct)
    (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh')
  
-inductive2 
+inductive 
   Beta :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
 where
   b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
@@ -85,7 +85,7 @@
    (auto intro!: simp add: abs_supp lam.supp subst_supp)
 
 lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"
-apply(ind_cases2 "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
+apply(ind_cases "Lam [a].t  \<longrightarrow>\<^isub>\<beta> t'")
 apply(auto simp add: lam.distinct lam.inject)
 apply(auto simp add: alpha)
 apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)
@@ -138,7 +138,7 @@
 
 (* valid contexts *)
 
-inductive2 
+inductive 
   valid :: "(name\<times>ty) list \<Rightarrow> bool"
 where
   v1[intro]: "valid []"
@@ -146,7 +146,7 @@
 
 equivariance valid 
 
-inductive_cases2 valid_elim[elim]: "valid ((a,\<tau>)#\<Gamma>)"
+inductive_cases valid_elim[elim]: "valid ((a,\<tau>)#\<Gamma>)"
 
 (* typing judgements *)
 
@@ -160,7 +160,7 @@
 apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
 done
 
-inductive2 
+inductive 
   typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60)
 where
   t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"
@@ -195,17 +195,17 @@
 
 constdefs
   "SN" :: "lam \<Rightarrow> bool"
-  "SN t \<equiv> termi Beta t"
+  "SN t \<equiv> termip Beta t"
 
 lemma SN_preserved: "\<lbrakk>SN(t1);t1\<longrightarrow>\<^isub>\<beta> t2\<rbrakk>\<Longrightarrow>SN(t2)"
 apply(simp add: SN_def)
-apply(drule_tac a="t2" in acc_downward)
+apply(drule_tac a="t2" in accp_downward)
 apply(auto)
 done
 
 lemma SN_intro: "(\<forall>t2. t1\<longrightarrow>\<^isub>\<beta>t2 \<longrightarrow> SN(t2))\<Longrightarrow>SN(t1)"
 apply(simp add: SN_def)
-apply(rule accI)
+apply(rule accp.accI)
 apply(auto)
 done
 
@@ -225,27 +225,27 @@
   "NEUT t \<equiv> (\<exists>a. t=Var a)\<or>(\<exists>t1 t2. t=App t1 t2)" 
 
 (* a slight hack to get the first element of applications *)
-inductive2 
+inductive 
   FST :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)
 where
   fst[intro!]:  "(App t s) \<guillemotright> t"
 
 lemma fst_elim[elim!]: 
   shows "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"
-apply(ind_cases2 "App t s \<guillemotright> t'")
+apply(ind_cases "App t s \<guillemotright> t'")
 apply(simp add: lam.inject)
 done
 
 lemma qq3: "SN(App t s)\<Longrightarrow>SN(t)"
 apply(simp add: SN_def)
-apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> termi Beta z")(*A*)
+apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> termip Beta z")(*A*)
 apply(force)
 (*A*)
-apply(erule acc_induct)
+apply(erule accp_induct)
 apply(clarify)
-apply(ind_cases2 "x \<guillemotright> z" for x z)
+apply(ind_cases "x \<guillemotright> z" for x z)
 apply(clarify)
-apply(rule accI)
+apply(rule accp.accI)
 apply(auto intro: b1)
 done
 
@@ -275,7 +275,7 @@
 lemma sub_ind: 
   "SN(u)\<Longrightarrow>(u\<in>RED \<tau>\<longrightarrow>(\<forall>t. (NEUT t\<and>CR2 \<tau>\<and>CR3 \<sigma>\<and>CR3_RED t (\<tau>\<rightarrow>\<sigma>))\<longrightarrow>(App t u)\<in>RED \<sigma>))"
 apply(simp add: SN_def)
-apply(erule acc_induct)
+apply(erule accp_induct)
 apply(auto)
 apply(simp add: CR3_def)
 apply(rotate_tac 5)
@@ -285,7 +285,7 @@
 apply(force simp only: NEUT_def)
 apply(simp (no_asm) add: CR3_RED_def)
 apply(clarify)
-apply(ind_cases2 "App t x \<longrightarrow>\<^isub>\<beta> t'" for x t t')
+apply(ind_cases "App t x \<longrightarrow>\<^isub>\<beta> t'" for x t t')
 apply(simp_all add: lam.inject)
 apply(simp only:  CR3_RED_def)
 apply(drule_tac x="s2" in spec)
@@ -360,29 +360,29 @@
 qed
     
 lemma double_acc_aux:
-  assumes a_acc: "acc r a"
-  and b_acc: "acc r b"
+  assumes a_acc: "accp r a"
+  and b_acc: "accp r b"
   and hyp: "\<And>x z.
-    (\<And>y. r y x \<Longrightarrow> acc r y) \<Longrightarrow>
+    (\<And>y. r y x \<Longrightarrow> accp r y) \<Longrightarrow>
     (\<And>y. r y x \<Longrightarrow> P y z) \<Longrightarrow>
-    (\<And>u. r u z \<Longrightarrow> acc r u) \<Longrightarrow>
+    (\<And>u. r u z \<Longrightarrow> accp r u) \<Longrightarrow>
     (\<And>u. r u z \<Longrightarrow> P x u) \<Longrightarrow> P x z"
   shows "P a b"
 proof -
   from a_acc
-  have r: "\<And>b. acc r b \<Longrightarrow> P a b"
-  proof (induct a rule: acc.induct)
+  have r: "\<And>b. accp r b \<Longrightarrow> P a b"
+  proof (induct a rule: accp.induct)
     case (accI x)
     note accI' = accI
-    have "acc r b" by fact
+    have "accp r b" by fact
     thus ?case
-    proof (induct b rule: acc.induct)
+    proof (induct b rule: accp.induct)
       case (accI y)
       show ?case
 	apply (rule hyp)
 	apply (erule accI')
 	apply (erule accI')
-	apply (rule acc.accI)
+	apply (rule accp.accI)
 	apply (erule accI)
 	apply (erule accI)
 	apply (erule accI)
@@ -393,7 +393,7 @@
 qed
 
 lemma double_acc:
-  "\<lbrakk>acc r a; acc r b; \<forall>x z. ((\<forall>y. r y x \<longrightarrow> P y z) \<and> (\<forall>u. r u z \<longrightarrow> P x u)) \<longrightarrow> P x z\<rbrakk> \<Longrightarrow> P a b"
+  "\<lbrakk>accp r a; accp r b; \<forall>x z. ((\<forall>y. r y x \<longrightarrow> P y z) \<and> (\<forall>u. r u z \<longrightarrow> P x u)) \<longrightarrow> P x z\<rbrakk> \<Longrightarrow> P a b"
 apply(rule_tac r="r" in double_acc_aux)
 apply(assumption)+
 apply(blast)
@@ -402,7 +402,7 @@
 lemma abs_RED: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"
 apply(simp)
 apply(clarify)
-apply(subgoal_tac "termi Beta t")(*1*)
+apply(subgoal_tac "termip Beta t")(*1*)
 apply(erule rev_mp)
 apply(subgoal_tac "u \<in> RED \<tau>")(*A*)
 apply(erule rev_mp)
@@ -423,7 +423,7 @@
 apply(force simp add: NEUT_def)
 apply(simp add: CR3_RED_def)
 apply(clarify)
-apply(ind_cases2 "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'" for xa z t')
+apply(ind_cases "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'" for xa z t')
 apply(auto simp add: lam.inject lam.distinct)
 apply(drule beta_abs)
 apply(auto)
@@ -472,7 +472,7 @@
 apply(force simp add: NEUT_def)
 apply(simp add: NORMAL_def)
 apply(clarify)
-apply(ind_cases2 "Var x \<longrightarrow>\<^isub>\<beta> t'" for t')
+apply(ind_cases "Var x \<longrightarrow>\<^isub>\<beta> t'" for t')
 apply(auto simp add: lam.inject lam.distinct)
 apply(force simp add: RED_props)
 apply(simp add: id_subs)
diff -r 90bccef65004 -r aca2c7f80e2f src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Wed Jul 11 11:35:17 2007 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Wed Jul 11 11:36:06 2007 +0200
@@ -207,7 +207,7 @@
 
 text {* Typing-Judgements *}
 
-inductive2
+inductive
   valid :: "(name \<times> 'a::pt_name) list \<Rightarrow> bool"
 where
     v_nil[intro]:  "valid []"
@@ -215,7 +215,7 @@
 
 equivariance valid 
 
-inductive_cases2  
+inductive_cases  
   valid_cons_inv_auto[elim]:"valid ((x,T)#\<Gamma>)"
 
 abbreviation
@@ -253,7 +253,7 @@
 ultimately show ?thesis by auto
 qed
 
-inductive2
+inductive
   typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
 where
   t_Var[intro]:   "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
@@ -287,7 +287,7 @@
 declare data.inject [simp add]
 
 
-inductive_cases2 typing_inv_auto[elim]: 
+inductive_cases typing_inv_auto[elim]: 
   "\<Gamma> \<turnstile> Lam [x].t : T"
   "\<Gamma> \<turnstile> Var x : T"
   "\<Gamma> \<turnstile> App x y : T"
@@ -487,7 +487,7 @@
 
 text {* Big-Step Evaluation *}
 
-inductive2
+inductive
   big :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) 
 where
   b_Lam[intro]:   "Lam [x].e \<Down> Lam [x].e"
@@ -530,7 +530,7 @@
 declare ty.inject  [simp add]
 declare data.inject [simp add]
 
-inductive_cases2 b_inv_auto[elim]: 
+inductive_cases b_inv_auto[elim]: 
   "App e\<^isub>1 e\<^isub>2 \<Down> t" 
   "Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 \<Down> t"
   "Lam[x].t \<Down> t"
@@ -615,7 +615,7 @@
   apply(assumption)
 done
 
-inductive2
+inductive
   val :: "trm\<Rightarrow>bool" 
 where
   v_Lam[intro]:   "val (Lam [x].e)"
@@ -628,7 +628,7 @@
 declare ty.inject  [simp add]
 declare data.inject [simp add]
 
-inductive_cases2 v_inv_auto[elim]: 
+inductive_cases v_inv_auto[elim]: 
   "val (Const n)"
   "val (Pr e\<^isub>1 e\<^isub>2)"
   "val (InL e)"
diff -r 90bccef65004 -r aca2c7f80e2f src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Wed Jul 11 11:35:17 2007 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Wed Jul 11 11:36:06 2007 +0200
@@ -27,7 +27,7 @@
 
 text {* valid contexts *}
 
-inductive2
+inductive
   valid :: "(name\<times>ty) list \<Rightarrow> bool"
 where
     v1[intro]: "valid []"
@@ -36,7 +36,7 @@
 equivariance valid
 
 text{* typing judgements *}
-inductive2
+inductive
   typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
 where
     t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"