# HG changeset patch
# User urbanc
# Date 1211466881 -7200
# Node ID 071f40487734ba9885e936d69a02e0b7acc12e5b
# Parent  003b5781b845fac154e8a0c33c0f9e8fd552cb3b
made the naming of the induction principles consistent: weak_induct is
induct and induct is strong_induct

diff -r 003b5781b845 -r 071f40487734 src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/CR.thy	Thu May 22 16:34:41 2008 +0200
@@ -10,7 +10,7 @@
   assumes asm: "x\<sharp>L"
   shows "L[x::=P] = L"
 using asm
-proof (nominal_induct L avoiding: x P rule: lam.induct)
+proof (nominal_induct L avoiding: x P rule: lam.strong_induct)
   case (Var z)
   have "x\<sharp>Var z" by fact
   thus "(Var z)[x::=P] = (Var z)" by (simp add: fresh_atm)
@@ -36,7 +36,7 @@
   assumes asm: "x\<sharp>L"
   shows "L[x::=P] = L"
   using asm 
-by (nominal_induct L avoiding: x P rule: lam.induct)
+by (nominal_induct L avoiding: x P rule: lam.strong_induct)
    (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_fact: 
@@ -44,7 +44,7 @@
   assumes asms: "z\<sharp>N" "z\<sharp>L"
   shows "z\<sharp>(N[y::=L])"
 using asms
-proof (nominal_induct N avoiding: z y L rule: lam.induct)
+proof (nominal_induct N avoiding: z y L rule: lam.strong_induct)
   case (Var u)
   have "z\<sharp>(Var u)" "z\<sharp>L" by fact+
   thus "z\<sharp>((Var u)[y::=L])" by simp
@@ -73,7 +73,7 @@
   assumes asms: "z\<sharp>N" "z\<sharp>L"
   shows "z\<sharp>(N[y::=L])"
   using asms 
-by (nominal_induct N avoiding: z y L rule: lam.induct)
+by (nominal_induct N avoiding: z y L rule: lam.strong_induct)
    (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_fact': 
@@ -81,7 +81,7 @@
   assumes a: "a\<sharp>t2"
   shows "a\<sharp>t1[a::=t2]"
 using a 
-by (nominal_induct t1 avoiding: a t2 rule: lam.induct)
+by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
    (auto simp add: abs_fresh fresh_atm)
 
 lemma substitution_lemma:  
@@ -89,7 +89,7 @@
   and     b: "x\<sharp>L"
   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
 using a b
-proof (nominal_induct M avoiding: x y N L rule: lam.induct)
+proof (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
   case (Var z) (* case 1: Variables*)
   have "x\<noteq>y" by fact
   have "x\<sharp>L" by fact
@@ -142,7 +142,7 @@
   assumes asm: "x\<noteq>y" "x\<sharp>L"
   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
   using asm 
-by (nominal_induct M avoiding: x y N L rule: lam.induct)
+by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
    (auto simp add: fresh_fact forget)
 
 section {* Beta Reduction *}
@@ -261,7 +261,7 @@
   assumes a: "c\<sharp>t1"
   shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
 using a
-by (nominal_induct t1 avoiding: a c t2 rule: lam.induct)
+by (nominal_induct t1 avoiding: a c t2 rule: lam.strong_induct)
    (auto simp add: calc_atm fresh_atm abs_fresh)
 
 lemma one_abs: 
@@ -295,7 +295,7 @@
   assumes a: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
 using a
-proof (nominal_induct M avoiding: x N N' rule: lam.induct)
+proof (nominal_induct M avoiding: x N N' rule: lam.strong_induct)
   case (Var y) 
   thus "Var y[x::=N] \<longrightarrow>\<^isub>1 Var y[x::=N']" by (cases "x=y") auto
 next
@@ -310,7 +310,7 @@
   assumes a: "N\<longrightarrow>\<^isub>1N'"
   shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
 using a
-by (nominal_induct M avoiding: x N N' rule: lam.induct)
+by (nominal_induct M avoiding: x N N' rule: lam.strong_induct)
    (auto simp add: fresh_prod fresh_atm)
 
 lemma one_subst: 
diff -r 003b5781b845 -r 071f40487734 src/HOL/Nominal/Examples/CR_Takahashi.thy
--- a/src/HOL/Nominal/Examples/CR_Takahashi.thy	Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy	Thu May 22 16:34:41 2008 +0200
@@ -36,31 +36,31 @@
  
 lemma  subst_eqvt[eqvt]:
   fixes pi::"name prm"
-  shows "pi\<bullet>t1[x::=t2] = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]"
-by (nominal_induct t1 avoiding: x t2 rule: lam.induct)
+  shows "pi\<bullet>(t1[x::=t2]) = (pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)]"
+by (nominal_induct t1 avoiding: x t2 rule: lam.strong_induct)
    (auto simp add: perm_bij fresh_atm fresh_bij)
 
 lemma forget:
   shows "x\<sharp>t \<Longrightarrow> t[x::=s] = t"
-by (nominal_induct t avoiding: x s rule: lam.induct)
+by (nominal_induct t avoiding: x s rule: lam.strong_induct)
    (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_fact:
   fixes z::"name"
-  shows "z\<sharp>s \<and> (z=y \<or> z\<sharp>t) \<Longrightarrow> z\<sharp>t[y::=s]"
-by (nominal_induct t avoiding: z y s rule: lam.induct)
+  shows "\<lbrakk>z\<sharp>s; (z=y \<or> z\<sharp>t)\<rbrakk> \<Longrightarrow> z\<sharp>t[y::=s]"
+by (nominal_induct t avoiding: z y s rule: lam.strong_induct)
    (auto simp add: abs_fresh fresh_prod fresh_atm)
 
 lemma substitution_lemma:  
   assumes a: "x\<noteq>y" "x\<sharp>u"
   shows "t[x::=s][y::=u] = t[y::=u][x::=s[y::=u]]"
-using a by (nominal_induct t avoiding: x y s u rule: lam.induct)
+using a by (nominal_induct t avoiding: x y s u rule: lam.strong_induct)
            (auto simp add: fresh_fact forget)
 
 lemma subst_rename: 
   assumes a: "y\<sharp>t"
   shows "t[x::=s] = ([(y,x)]\<bullet>t)[y::=s]"
-using a by (nominal_induct t avoiding: x y s rule: lam.induct)
+using a by (nominal_induct t avoiding: x y s rule: lam.strong_induct)
            (auto simp add: calc_atm fresh_atm abs_fresh)
 
 section {* Beta-Reduction *}
@@ -98,7 +98,7 @@
 
 lemma One_refl:
   shows "t \<longrightarrow>\<^isub>1 t"
-by (nominal_induct t rule: lam.induct) (auto)
+by (nominal_induct t rule: lam.strong_induct) (auto)
 
 lemma One_subst: 
   assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2"
@@ -136,12 +136,6 @@
          (\<exists>x p p' s'. r = p'[x::=s'] \<and> t = Lam [x].p \<and> p \<longrightarrow>\<^isub>1 p' \<and> s \<longrightarrow>\<^isub>1 s' \<and> x\<sharp>(s,s'))" 
 using a by (cases rule: One.cases) (auto simp add: lam.inject)
 
-lemma One_App_: 
-  assumes a: "App t s \<longrightarrow>\<^isub>1 r"
-  obtains t' s' where "r = App t' s'" "t \<longrightarrow>\<^isub>1 t'" "s \<longrightarrow>\<^isub>1 s'" 
-        | x p p' s' where "r = p'[x::=s']" "t = Lam [x].p" "p \<longrightarrow>\<^isub>1 p'" "s \<longrightarrow>\<^isub>1 s'" "x\<sharp>(s,s')"
-using a by (cases rule: One.cases) (auto simp add: lam.inject)
-
 lemma One_Redex: 
   assumes a: "App (Lam [x].t) s \<longrightarrow>\<^isub>1 r" "x\<sharp>(s,r)"
   shows "(\<exists>t' s'. r = App (Lam [x].t') s' \<and> t \<longrightarrow>\<^isub>1 t' \<and> s \<longrightarrow>\<^isub>1 s') \<or> 
@@ -205,9 +199,10 @@
 
 lemma Development_existence:
   shows "\<exists>M'. M \<longrightarrow>\<^isub>d M'"
-by (nominal_induct M rule: lam.induct)
+by (nominal_induct M rule: lam.strong_induct)
    (auto dest!: Dev_Lam intro: better_d4_intro)
 
+(* needs fixing *)
 lemma Triangle:
   assumes a: "t \<longrightarrow>\<^isub>d t1" "t \<longrightarrow>\<^isub>1 t2"
   shows "t2 \<longrightarrow>\<^isub>1 t1"
@@ -220,7 +215,7 @@
   have "App (Lam [x].t1) s1 \<longrightarrow>\<^isub>1 t2" by fact
   then obtain t' s' where "(t2 = App (Lam [x].t') s' \<and> t1 \<longrightarrow>\<^isub>1 t' \<and> s1 \<longrightarrow>\<^isub>1 s') \<or> 
                            (t2 = t'[x::=s'] \<and> t1 \<longrightarrow>\<^isub>1 t' \<and> s1 \<longrightarrow>\<^isub>1 s')"
-    (* MARKUS: How does I do this better *) using fc by (auto dest!: One_Redex)
+  using fc by (auto dest!: One_Redex)
   then show "t2 \<longrightarrow>\<^isub>1 t1'[x::=s2]"
     apply -
     apply(erule disjE)
@@ -282,19 +277,13 @@
   shows "t \<longrightarrow>\<^isub>\<beta>\<^sup>* s"
 using a by (induct) (auto intro!: Beta_congs)
 
-lemma One_star_Lam_cong: 
+lemma One_congs: 
   assumes a: "t1 \<longrightarrow>\<^isub>1\<^sup>* t2" 
   shows "Lam [x].t1 \<longrightarrow>\<^isub>1\<^sup>* Lam [x].t2"
-using a by (induct) (auto)
-
-lemma One_star_App_cong: 
-  assumes a: "t1 \<longrightarrow>\<^isub>1\<^sup>* t2" 
-  shows "App t1 s \<longrightarrow>\<^isub>1\<^sup>* App t2 s"
+  and   "App t1 s \<longrightarrow>\<^isub>1\<^sup>* App t2 s"
   and   "App s t1 \<longrightarrow>\<^isub>1\<^sup>* App s t2"
 using a by (induct) (auto intro: One_refl)
 
-lemmas One_congs = One_star_App_cong One_star_Lam_cong
-
 lemma Beta_implies_One_star: 
   assumes a: "t1 \<longrightarrow>\<^isub>\<beta> t2" 
   shows "t1 \<longrightarrow>\<^isub>1\<^sup>* t2"
diff -r 003b5781b845 -r 071f40487734 src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy	Thu May 22 16:34:41 2008 +0200
@@ -30,14 +30,14 @@
 lemma ty_cases:
   fixes T::ty
   shows "(\<exists>s. T=PR s) \<or> (\<exists>T'. T=NOT T') \<or> (\<exists>S U. T=S OR U) \<or> (\<exists>S U. T=S AND U) \<or> (\<exists>S U. T=S IMP U)"
-by (induct T rule:ty.weak_induct) (auto)
+by (induct T rule:ty.induct) (auto)
 
 lemma fresh_ty:
   fixes a::"coname"
   and   x::"name"
   and   T::"ty"
   shows "a\<sharp>T" and "x\<sharp>T"
-by (nominal_induct T rule: ty.induct)
+by (nominal_induct T rule: ty.strong_induct)
    (auto simp add: fresh_string)
 
 text {* terms *}
@@ -117,28 +117,28 @@
 lemma crename_name_eqvt[eqvt]:
   fixes pi::"name prm"
   shows "pi\<bullet>(M[d\<turnstile>c>e]) = (pi\<bullet>M)[(pi\<bullet>d)\<turnstile>c>(pi\<bullet>e)]"
-apply(nominal_induct M avoiding: d e rule: trm.induct)
+apply(nominal_induct M avoiding: d e rule: trm.strong_induct)
 apply(auto simp add: fresh_bij eq_bij)
 done
 
 lemma crename_coname_eqvt[eqvt]:
   fixes pi::"coname prm"
   shows "pi\<bullet>(M[d\<turnstile>c>e]) = (pi\<bullet>M)[(pi\<bullet>d)\<turnstile>c>(pi\<bullet>e)]"
-apply(nominal_induct M avoiding: d e rule: trm.induct)
+apply(nominal_induct M avoiding: d e rule: trm.strong_induct)
 apply(auto simp add: fresh_bij eq_bij)
 done
 
 lemma nrename_name_eqvt[eqvt]:
   fixes pi::"name prm"
   shows "pi\<bullet>(M[x\<turnstile>n>y]) = (pi\<bullet>M)[(pi\<bullet>x)\<turnstile>n>(pi\<bullet>y)]"
-apply(nominal_induct M avoiding: x y rule: trm.induct)
+apply(nominal_induct M avoiding: x y rule: trm.strong_induct)
 apply(auto simp add: fresh_bij eq_bij)
 done
 
 lemma nrename_coname_eqvt[eqvt]:
   fixes pi::"coname prm"
   shows "pi\<bullet>(M[x\<turnstile>n>y]) = (pi\<bullet>M)[(pi\<bullet>x)\<turnstile>n>(pi\<bullet>y)]"
-apply(nominal_induct M avoiding: x y rule: trm.induct)
+apply(nominal_induct M avoiding: x y rule: trm.strong_induct)
 apply(auto simp add: fresh_bij eq_bij)
 done
 
@@ -148,57 +148,57 @@
   assumes a: "x\<sharp>M"
   shows "M[x\<turnstile>n>y] = M"
 using a
-by (nominal_induct M avoiding: x y rule: trm.induct)
+by (nominal_induct M avoiding: x y rule: trm.strong_induct)
    (auto simp add: trm.inject fresh_atm abs_fresh fin_supp abs_supp)
 
 lemma crename_fresh:
   assumes a: "a\<sharp>M"
   shows "M[a\<turnstile>c>b] = M"
 using a
-by (nominal_induct M avoiding: a b rule: trm.induct)
+by (nominal_induct M avoiding: a b rule: trm.strong_induct)
    (auto simp add: trm.inject fresh_atm abs_fresh)
 
 lemma nrename_nfresh:
   fixes x::"name"
   shows "x\<sharp>y\<Longrightarrow>x\<sharp>M[x\<turnstile>n>y]"
-by (nominal_induct M avoiding: x y rule: trm.induct)
+by (nominal_induct M avoiding: x y rule: trm.strong_induct)
    (auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
 
  lemma crename_nfresh:
   fixes x::"name"
   shows "x\<sharp>M\<Longrightarrow>x\<sharp>M[a\<turnstile>c>b]"
-by (nominal_induct M avoiding: a b rule: trm.induct)
+by (nominal_induct M avoiding: a b rule: trm.strong_induct)
    (auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
 
 lemma crename_cfresh:
   fixes a::"coname"
   shows "a\<sharp>b\<Longrightarrow>a\<sharp>M[a\<turnstile>c>b]"
-by (nominal_induct M avoiding: a b rule: trm.induct)
+by (nominal_induct M avoiding: a b rule: trm.strong_induct)
    (auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
 
 lemma nrename_cfresh:
   fixes c::"coname"
   shows "c\<sharp>M\<Longrightarrow>c\<sharp>M[x\<turnstile>n>y]"
-by (nominal_induct M avoiding: x y rule: trm.induct)
+by (nominal_induct M avoiding: x y rule: trm.strong_induct)
    (auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
 
 lemma nrename_nfresh':
   fixes x::"name"
   shows "x\<sharp>(M,z,y)\<Longrightarrow>x\<sharp>M[z\<turnstile>n>y]"
-by (nominal_induct M avoiding: x z y rule: trm.induct)
+by (nominal_induct M avoiding: x z y rule: trm.strong_induct)
    (auto simp add: fresh_prod fresh_atm abs_fresh abs_supp fin_supp)
 
 lemma crename_cfresh':
   fixes a::"coname"
   shows "a\<sharp>(M,b,c)\<Longrightarrow>a\<sharp>M[b\<turnstile>c>c]"
-by (nominal_induct M avoiding: a b c rule: trm.induct)
+by (nominal_induct M avoiding: a b c rule: trm.strong_induct)
    (auto simp add: fresh_prod fresh_atm abs_fresh abs_supp fin_supp)
 
 lemma nrename_rename:
   assumes a: "x'\<sharp>M"
   shows "([(x',x)]\<bullet>M)[x'\<turnstile>n>y]= M[x\<turnstile>n>y]"
 using a
-apply(nominal_induct M avoiding: x x' y rule: trm.induct)
+apply(nominal_induct M avoiding: x x' y rule: trm.strong_induct)
 apply(auto simp add: abs_fresh fresh_bij fresh_atm fresh_prod fresh_right calc_atm abs_supp fin_supp)
 apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)
 done
@@ -207,7 +207,7 @@
   assumes a: "a'\<sharp>M"
   shows "([(a',a)]\<bullet>M)[a'\<turnstile>c>b]= M[a\<turnstile>c>b]"
 using a
-apply(nominal_induct M avoiding: a a' b rule: trm.induct)
+apply(nominal_induct M avoiding: a a' b rule: trm.strong_induct)
 apply(auto simp add: abs_fresh fresh_bij fresh_atm fresh_prod fresh_right calc_atm abs_supp fin_supp)
 apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)
 done
@@ -271,27 +271,27 @@
 
 lemma crename_id:
   shows "M[a\<turnstile>c>a] = M"
-by (nominal_induct M avoiding: a rule: trm.induct) (auto)
+by (nominal_induct M avoiding: a rule: trm.strong_induct) (auto)
 
 lemma nrename_id:
   shows "M[x\<turnstile>n>x] = M"
-by (nominal_induct M avoiding: x rule: trm.induct) (auto)
+by (nominal_induct M avoiding: x rule: trm.strong_induct) (auto)
 
 lemma nrename_swap:
   shows "x\<sharp>M \<Longrightarrow> [(x,y)]\<bullet>M = M[y\<turnstile>n>x]"
-by (nominal_induct M avoiding: x y rule: trm.induct) 
+by (nominal_induct M avoiding: x y rule: trm.strong_induct) 
    (simp_all add: calc_atm fresh_atm trm.inject alpha abs_fresh abs_supp fin_supp)
 
 lemma crename_swap:
   shows "a\<sharp>M \<Longrightarrow> [(a,b)]\<bullet>M = M[b\<turnstile>c>a]"
-by (nominal_induct M avoiding: a b rule: trm.induct) 
+by (nominal_induct M avoiding: a b rule: trm.strong_induct) 
    (simp_all add: calc_atm fresh_atm trm.inject alpha abs_fresh abs_supp fin_supp)
 
 lemma crename_ax:
   assumes a: "M[a\<turnstile>c>b] = Ax x c" "c\<noteq>a" "c\<noteq>b"
   shows "M = Ax x c"
 using a
-apply(nominal_induct M avoiding: a b x c rule: trm.induct)
+apply(nominal_induct M avoiding: a b x c rule: trm.strong_induct)
 apply(simp_all add: trm.inject split: if_splits)
 done
 
@@ -299,7 +299,7 @@
   assumes a: "M[x\<turnstile>n>y] = Ax z a" "z\<noteq>x" "z\<noteq>y"
   shows "M = Ax z a"
 using a
-apply(nominal_induct M avoiding: x y z a rule: trm.induct)
+apply(nominal_induct M avoiding: x y z a rule: trm.strong_induct)
 apply(simp_all add: trm.inject split: if_splits)
 done
 
@@ -917,7 +917,7 @@
   and   pi2::"coname prm"
   shows "pi1\<bullet>(M{c:=(x).N}) = (pi1\<bullet>M){(pi1\<bullet>c):=(pi1\<bullet>x).(pi1\<bullet>N)}"
   and   "pi2\<bullet>(M{c:=(x).N}) = (pi2\<bullet>M){(pi2\<bullet>c):=(pi2\<bullet>x).(pi2\<bullet>N)}"
-apply(nominal_induct M avoiding: c x N rule: trm.induct)
+apply(nominal_induct M avoiding: c x N rule: trm.strong_induct)
 apply(auto simp add: eq_bij fresh_bij eqvts)
 apply(perm_simp)+
 done
@@ -927,14 +927,14 @@
   and   pi2::"coname prm"
   shows "pi1\<bullet>(M{x:=<c>.N}) = (pi1\<bullet>M){(pi1\<bullet>x):=<(pi1\<bullet>c)>.(pi1\<bullet>N)}"
   and   "pi2\<bullet>(M{x:=<c>.N}) = (pi2\<bullet>M){(pi2\<bullet>x):=<(pi2\<bullet>c)>.(pi2\<bullet>N)}"
-apply(nominal_induct M avoiding: c x N rule: trm.induct)
+apply(nominal_induct M avoiding: c x N rule: trm.strong_induct)
 apply(auto simp add: eq_bij fresh_bij eqvts)
 apply(perm_simp)+
 done
 
 lemma supp_subst1:
   shows "supp (M{y:=<c>.P}) \<subseteq> ((supp M) - {y}) \<union> (supp P)"
-apply(nominal_induct M avoiding: y P c rule: trm.induct)
+apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
 apply(auto)
 apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
@@ -1063,7 +1063,7 @@
 
 lemma supp_subst2:
   shows "supp (M{y:=<c>.P}) \<subseteq> supp (M) \<union> ((supp P) - {c})"
-apply(nominal_induct M avoiding: y P c rule: trm.induct)
+apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
 apply(auto)
 apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
@@ -1176,7 +1176,7 @@
 
 lemma supp_subst3:
   shows "supp (M{c:=(x).P}) \<subseteq> ((supp M) - {c}) \<union> (supp P)"
-apply(nominal_induct M avoiding: x P c rule: trm.induct)
+apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
 apply(auto)
 apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
@@ -1304,7 +1304,7 @@
 
 lemma supp_subst4:
   shows "supp (M{c:=(x).P}) \<subseteq> (supp M) \<union> ((supp P) - {x})"
-apply(nominal_induct M avoiding: x P c rule: trm.induct)
+apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
 apply(auto)
 apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
@@ -1409,7 +1409,7 @@
 
 lemma supp_subst5:
   shows "(supp M - {y}) \<subseteq> supp (M{y:=<c>.P})"
-apply(nominal_induct M avoiding: y P c rule: trm.induct)
+apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
 apply(auto)
 apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
@@ -1476,7 +1476,7 @@
 
 lemma supp_subst6:
   shows "(supp M) \<subseteq> ((supp (M{y:=<c>.P}))::coname set)"
-apply(nominal_induct M avoiding: y P c rule: trm.induct)
+apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
 apply(auto)
 apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
@@ -1543,7 +1543,7 @@
 
 lemma supp_subst7:
   shows "(supp M - {c}) \<subseteq>  supp (M{c:=(x).P})"
-apply(nominal_induct M avoiding: x P c rule: trm.induct)
+apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
 apply(auto)
 apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
@@ -1602,7 +1602,7 @@
 
 lemma supp_subst8:
   shows "(supp M) \<subseteq> ((supp (M{c:=(x).P}))::name set)"
-apply(nominal_induct M avoiding: x P c rule: trm.induct)
+apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
 apply(auto)
 apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
@@ -1681,7 +1681,7 @@
 lemma forget:
   shows "x\<sharp>M \<Longrightarrow> M{x:=<c>.P} = M"
   and   "c\<sharp>M \<Longrightarrow> M{c:=(x).P} = M"
-apply(nominal_induct M avoiding: x c P rule: trm.induct)
+apply(nominal_induct M avoiding: x c P rule: trm.strong_induct)
 apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
 done
 
@@ -1689,7 +1689,7 @@
   assumes a: "c\<sharp>(M,a)"
   shows "M{a:=(x).N} = ([(c,a)]\<bullet>M){c:=(x).N}"
 using a
-proof(nominal_induct M avoiding: c a x N rule: trm.induct)
+proof(nominal_induct M avoiding: c a x N rule: trm.strong_induct)
   case (Ax z d)
   then show ?case by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha)
 next
@@ -1784,7 +1784,7 @@
   assumes a: "y\<sharp>(N,x)"
   shows "M{a:=(x).N} = M{a:=(y).([(y,x)]\<bullet>N)}"
 using a
-proof(nominal_induct M avoiding: a x y N rule: trm.induct)
+proof(nominal_induct M avoiding: a x y N rule: trm.strong_induct)
   case (Ax z d)
   then show ?case 
     by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
@@ -1872,7 +1872,7 @@
   assumes a: "y\<sharp>(M,x)"
   shows "M{x:=<a>.N} = ([(y,x)]\<bullet>M){y:=<a>.N}"
 using a
-proof(nominal_induct M avoiding: a x y N rule: trm.induct)
+proof(nominal_induct M avoiding: a x y N rule: trm.strong_induct)
   case (Ax z d)
   then show ?case by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha)
 next
@@ -1962,7 +1962,7 @@
   assumes a: "c\<sharp>(N,a)"
   shows "M{x:=<a>.N} = M{x:=<c>.([(c,a)]\<bullet>N)}"
 using a
-proof(nominal_induct M avoiding: x c a N rule: trm.induct)
+proof(nominal_induct M avoiding: x c a N rule: trm.strong_induct)
   case (Ax z d)
   then show ?case 
     by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
@@ -2425,7 +2425,7 @@
   assumes a: "c\<noteq>a" "c\<noteq>b"
   shows "M{x:=<c>.P}[a\<turnstile>c>b] = M[a\<turnstile>c>b]{x:=<c>.(P[a\<turnstile>c>b])}"
 using a
-apply(nominal_induct M avoiding: x c P a b rule: trm.induct)
+apply(nominal_induct M avoiding: x c P a b rule: trm.strong_induct)
 apply(auto simp add: subst_fresh rename_fresh trm.inject)
 apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,x,c)")
 apply(erule exE)
@@ -2517,7 +2517,7 @@
   assumes a: "c\<noteq>a" "c\<noteq>b"
   shows "M{c:=(x).P}[a\<turnstile>c>b] = M[a\<turnstile>c>b]{c:=(x).(P[a\<turnstile>c>b])}"
 using a
-apply(nominal_induct M avoiding: x c P a b rule: trm.induct)
+apply(nominal_induct M avoiding: x c P a b rule: trm.strong_induct)
 apply(auto simp add: subst_fresh rename_fresh trm.inject)
 apply(rule trans)
 apply(rule better_crename_Cut)
@@ -2591,7 +2591,7 @@
   assumes a: "x\<noteq>y" "x\<noteq>z"
   shows "M{x:=<c>.P}[y\<turnstile>n>z] = M[y\<turnstile>n>z]{x:=<c>.(P[y\<turnstile>n>z])}"
 using a
-apply(nominal_induct M avoiding: x c P y z rule: trm.induct)
+apply(nominal_induct M avoiding: x c P y z rule: trm.strong_induct)
 apply(auto simp add: subst_fresh rename_fresh trm.inject)
 apply(rule trans)
 apply(rule better_nrename_Cut)
@@ -2663,7 +2663,7 @@
   assumes a: "x\<noteq>y" "x\<noteq>z"
   shows "M{c:=(x).P}[y\<turnstile>n>z] = M[y\<turnstile>n>z]{c:=(x).(P[y\<turnstile>n>z])}"
 using a
-apply(nominal_induct M avoiding: x c P y z rule: trm.induct)
+apply(nominal_induct M avoiding: x c P y z rule: trm.strong_induct)
 apply(auto simp add: subst_fresh rename_fresh trm.inject)
 apply(rule trans)
 apply(rule better_nrename_Cut)
@@ -3031,7 +3031,7 @@
   assumes a: "\<not>(fin M x)" 
   shows "\<not>(fin (M{c:=(y).P}) x)"
 using a
-apply(nominal_induct M avoiding: x c y P rule: trm.induct)
+apply(nominal_induct M avoiding: x c y P rule: trm.strong_induct)
 apply(auto)
 apply(drule fin_elims, simp)
 apply(drule fin_elims, simp)
@@ -3116,7 +3116,7 @@
   assumes a: "\<not>(fin M x)" 
   shows "\<not>(fin (M{y:=<c>.P}) x)"
 using a
-apply(nominal_induct M avoiding: x c y P rule: trm.induct)
+apply(nominal_induct M avoiding: x c y P rule: trm.strong_induct)
 apply(auto)
 apply(erule fin.cases, simp_all add: trm.inject)
 apply(erule fin.cases, simp_all add: trm.inject)
@@ -3204,7 +3204,7 @@
   assumes a: "fin M x" "x\<noteq>y" "x\<sharp>P"
   shows "fin (M{y:=<c>.P}) x"
 using a
-apply(nominal_induct M avoiding: x y c P rule: trm.induct)
+apply(nominal_induct M avoiding: x y c P rule: trm.strong_induct)
 apply(auto dest!: fin_elims simp add: subst_fresh abs_fresh)
 apply(rule fin.intros, simp add: subst_fresh abs_fresh)
 apply(rule fin.intros, simp add: subst_fresh abs_fresh)
@@ -3221,7 +3221,7 @@
   assumes a: "fin M y" "x\<noteq>y" "y\<sharp>P" "M\<noteq>Ax y c" 
   shows "fin (M{c:=(x).P}) y"
 using a
-apply(nominal_induct M avoiding: x y c P rule: trm.induct)
+apply(nominal_induct M avoiding: x y c P rule: trm.strong_induct)
 apply(drule fin_elims)
 apply(simp add: trm.inject)
 apply(rule fin.intros)
@@ -3268,7 +3268,7 @@
   assumes a: "fin M x" "x\<noteq>y" "x\<sharp>P"
   shows "M[x\<turnstile>n>y]{y:=<c>.P} = Cut <c>.P (x).(M{y:=<c>.P})"
 using a
-apply(nominal_induct M avoiding: x y c P rule: trm.induct)
+apply(nominal_induct M avoiding: x y c P rule: trm.strong_induct)
 apply(drule fin_Ax_elim)
 apply(simp)
 apply(simp add: trm.inject)
@@ -3454,7 +3454,7 @@
   assumes a: "\<not>(fic M a)" 
   shows "\<not>(fic (M{y:=<c>.P}) a)"
 using a
-apply(nominal_induct M avoiding: a c y P rule: trm.induct)
+apply(nominal_induct M avoiding: a c y P rule: trm.strong_induct)
 apply(auto)
 apply(drule fic_elims, simp)
 apply(drule fic_elims, simp)
@@ -3530,7 +3530,7 @@
   assumes a: "\<not>(fic M a)" 
   shows "\<not>(fic (M{c:=(y).P}) a)"
 using a
-apply(nominal_induct M avoiding: a c y P rule: trm.induct)
+apply(nominal_induct M avoiding: a c y P rule: trm.strong_induct)
 apply(auto)
 apply(drule fic_elims, simp)
 apply(drule fic_elims, simp)
@@ -3612,7 +3612,7 @@
   assumes a: "fic M a" "a\<noteq>b" "a\<sharp>P"
   shows "fic (M{b:=(x).P}) a"
 using a
-apply(nominal_induct M avoiding: x b a P rule: trm.induct)
+apply(nominal_induct M avoiding: x b a P rule: trm.strong_induct)
 apply(drule fic_elims)
 apply(simp add: fic.intros)
 apply(drule fic_elims, simp)
@@ -3655,7 +3655,7 @@
   assumes a: "fic M a" "c\<noteq>a" "a\<sharp>P" "M\<noteq>Ax x a" 
   shows "fic (M{x:=<c>.P}) a"
 using a
-apply(nominal_induct M avoiding: x a c P rule: trm.induct)
+apply(nominal_induct M avoiding: x a c P rule: trm.strong_induct)
 apply(drule fic_elims)
 apply(simp add: trm.inject)
 apply(rule fic.intros)
@@ -3699,7 +3699,7 @@
   assumes a: "fic M a" "a\<noteq>b" "a\<sharp>P"
   shows "M[a\<turnstile>c>b]{b:=(y).P} = Cut <a>.(M{b:=(y).P}) (y).P"
 using a
-apply(nominal_induct M avoiding: a b  y P rule: trm.induct)
+apply(nominal_induct M avoiding: a b  y P rule: trm.strong_induct)
 apply(drule fic_Ax_elim)
 apply(simp)
 apply(simp add: trm.inject)
@@ -5455,7 +5455,7 @@
 
 lemma subst_not_fin1:
   shows "\<not>fin(M{x:=<c>.P}) x"
-apply(nominal_induct M avoiding: x c P rule: trm.induct)
+apply(nominal_induct M avoiding: x c P rule: trm.strong_induct)
 apply(auto)
 apply(drule fin_elims, simp)
 apply(drule fin_elims, simp)
@@ -5512,7 +5512,7 @@
   assumes a: "\<not>fin M y"
   shows "\<not>fin(M{c:=(x).P}) y" 
 using a
-apply(nominal_induct M avoiding: x c P y rule: trm.induct)
+apply(nominal_induct M avoiding: x c P y rule: trm.strong_induct)
 apply(auto)
 apply(drule fin_elims, simp)
 apply(drule fin_elims, simp)
@@ -5587,7 +5587,7 @@
 
 lemma subst_not_fic1:
   shows "\<not>fic (M{a:=(x).P}) a"
-apply(nominal_induct M avoiding: a x P rule: trm.induct)
+apply(nominal_induct M avoiding: a x P rule: trm.strong_induct)
 apply(auto)
 apply(erule fic.cases, simp_all add: trm.inject)
 apply(erule fic.cases, simp_all add: trm.inject)
@@ -5644,7 +5644,7 @@
   assumes a: "\<not>fic M a"
   shows "\<not>fic(M{x:=<b>.P}) a" 
 using a
-apply(nominal_induct M avoiding: x a P b rule: trm.induct)
+apply(nominal_induct M avoiding: x a P b rule: trm.strong_induct)
 apply(auto)
 apply(drule fic_elims, simp)
 apply(drule fic_elims, simp)
@@ -5858,7 +5858,7 @@
 
 lemma subst_with_ax1:
   shows "M{x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* M[x\<turnstile>n>y]"
-proof(nominal_induct M avoiding: x a y rule: trm.induct)
+proof(nominal_induct M avoiding: x a y rule: trm.strong_induct)
   case (Ax z b x a y)
   show "(Ax z b){x:=<a>.Ax y a} \<longrightarrow>\<^isub>a* (Ax z b)[x\<turnstile>n>y]"
   proof (cases "z=x")
@@ -6115,7 +6115,7 @@
 
 lemma subst_with_ax2:
   shows "M{b:=(x).Ax x a} \<longrightarrow>\<^isub>a* M[b\<turnstile>c>a]"
-proof(nominal_induct M avoiding: b a x rule: trm.induct)
+proof(nominal_induct M avoiding: b a x rule: trm.strong_induct)
   case (Ax z c b a x)
   show "(Ax z c){b:=(x).Ax x a} \<longrightarrow>\<^isub>a* (Ax z c)[b\<turnstile>c>a]"
   proof (cases "c=b")
@@ -6371,7 +6371,7 @@
 
 lemma not_Ax1:
   shows "\<not>(b\<sharp>M) \<Longrightarrow> M{b:=(y).Q} \<noteq> Ax x a"
-apply(nominal_induct M avoiding: b y Q x a rule: trm.induct)
+apply(nominal_induct M avoiding: b y Q x a rule: trm.strong_induct)
 apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
 apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm{coname:=(y).Q},Q)")
 apply(erule exE)
@@ -6443,7 +6443,7 @@
 
 lemma not_Ax2:
   shows "\<not>(x\<sharp>M) \<Longrightarrow> M{x:=<b>.Q} \<noteq> Ax y a"
-apply(nominal_induct M avoiding: b y Q x a rule: trm.induct)
+apply(nominal_induct M avoiding: b y Q x a rule: trm.strong_induct)
 apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
 apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<b>.Q},Q)")
 apply(erule exE)
@@ -6523,7 +6523,7 @@
   assumes a: "x\<noteq>y" "x\<sharp>P" "y\<sharp>P" 
   shows "N{y:=<c>.P}{x:=<c>.P} = N{x:=<c>.Ax y c}{y:=<c>.P}"
 using a
-proof(nominal_induct N avoiding: x y c P rule: trm.induct)
+proof(nominal_induct N avoiding: x y c P rule: trm.strong_induct)
   case Ax
   then show ?case
     by (auto simp add: abs_fresh fresh_atm forget trm.inject)
@@ -6831,7 +6831,7 @@
   assumes a: "a\<noteq>b" "a\<sharp>P" "b\<sharp>P" 
   shows "N{a:=(y).P}{b:=(y).P} = N{b:=(y).Ax y a}{a:=(y).P}"
 using a
-proof(nominal_induct N avoiding: a b y P rule: trm.induct)
+proof(nominal_induct N avoiding: a b y P rule: trm.strong_induct)
   case Ax
   then show ?case
     by (auto simp add: abs_fresh fresh_atm forget trm.inject)
@@ -7118,7 +7118,7 @@
   assumes a: "a\<sharp>(Q,b)" "x\<sharp>(y,P,Q)" "b\<sharp>Q" "y\<sharp>P" 
   shows "M{x:=<a>.P}{b:=(y).Q} = M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}"
 using a
-proof(nominal_induct M avoiding: x a P b y Q rule: trm.induct)
+proof(nominal_induct M avoiding: x a P b y Q rule: trm.strong_induct)
   case (Ax z c)
   have fs: "a\<sharp>(Q,b)" "x\<sharp>(y,P,Q)" "b\<sharp>Q" "y\<sharp>P" by fact+
   { assume asm: "z=x \<and> c=b"
@@ -7407,7 +7407,7 @@
   assumes a: "a\<sharp>(b,P,N)" "x\<sharp>(y,P,M)" "b\<sharp>(M,N)" "y\<sharp>P"
   shows "M{a:=(x).N}{y:=<b>.P} = M{y:=<b>.P}{a:=(x).N{y:=<b>.P}}"
 using a
-proof(nominal_induct M avoiding: a x N y b P rule: trm.induct)
+proof(nominal_induct M avoiding: a x N y b P rule: trm.strong_induct)
   case (Ax z c)
   then show ?case
     by (auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
@@ -7691,7 +7691,7 @@
   assumes a: "a\<sharp>(P,N,c)" "c\<sharp>(M,N)" "x\<sharp>(y,P,M)" "y\<sharp>(P,x)" "M\<noteq>Ax y a"
   shows "N{x:=<a>.M}{y:=<c>.P} = N{y:=<c>.P}{x:=<a>.(M{y:=<c>.P})}"
 using a
-proof(nominal_induct N avoiding: x y a c M P rule: trm.induct)
+proof(nominal_induct N avoiding: x y a c M P rule: trm.strong_induct)
   case (Ax z c)
   then show ?case
     by(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
@@ -7960,7 +7960,7 @@
   assumes a: "x\<sharp>(P,N,y)" "y\<sharp>(M,N)" "a\<sharp>(c,P,M)" "c\<sharp>(P,a)" "M\<noteq>Ax x c"
   shows "N{a:=(x).M}{c:=(y).P} = N{c:=(y).P}{a:=(x).(M{c:=(y).P})}"
 using a
-proof(nominal_induct N avoiding: x y a c M P rule: trm.induct)
+proof(nominal_induct N avoiding: x y a c M P rule: trm.strong_induct)
   case (Ax z c)
   then show ?case
     by (auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
@@ -11177,12 +11177,12 @@
 
 lemma NEGn_decreasing:
   shows "X\<subseteq>Y \<Longrightarrow> NEGn B Y \<subseteq> NEGn B X"
-by (nominal_induct B rule: ty.induct)
+by (nominal_induct B rule: ty.strong_induct)
    (auto dest: BINDINGn_decreasing)
 
 lemma NEGc_decreasing:
   shows "X\<subseteq>Y \<Longrightarrow> NEGc B Y \<subseteq> NEGc B X"
-by (nominal_induct B rule: ty.induct)
+by (nominal_induct B rule: ty.strong_induct)
    (auto dest: BINDINGc_decreasing)
 
 lemma mono_NEGn_NEGc:
@@ -11246,11 +11246,11 @@
   and   "AXIOMSc B \<subseteq> (\<parallel><B>\<parallel>)"
 proof -
   have "AXIOMSn B \<subseteq> NEGn B (\<parallel><B>\<parallel>)"
-    by (nominal_induct B rule: ty.induct) (auto)
+    by (nominal_induct B rule: ty.strong_induct) (auto)
   then show "AXIOMSn B \<subseteq> \<parallel>(B)\<parallel>" using NEG_simp by blast
 next
   have "AXIOMSc B \<subseteq> NEGc B (\<parallel>(B)\<parallel>)"
-    by (nominal_induct B rule: ty.induct) (auto)
+    by (nominal_induct B rule: ty.strong_induct) (auto)
   then show "AXIOMSc B \<subseteq> \<parallel><B>\<parallel>" using NEG_simp by blast
 qed
 
@@ -11445,7 +11445,7 @@
   fixes pi::"name prm"
   shows   "(pi\<bullet>(\<parallel>(B)\<parallel>)) = (\<parallel>(B)\<parallel>)"
   and     "(pi\<bullet>(\<parallel><B>\<parallel>)) = (\<parallel><B>\<parallel>)"
-proof (nominal_induct B rule: ty.induct)
+proof (nominal_induct B rule: ty.strong_induct)
   case (PR X)
   { case 1 show ?case 
       apply -
@@ -11555,7 +11555,7 @@
   fixes pi::"coname prm"
   shows   "(pi\<bullet>(\<parallel>(B)\<parallel>)) = (\<parallel>(B)\<parallel>)"
   and     "(pi\<bullet>(\<parallel><B>\<parallel>)) = (\<parallel><B>\<parallel>)"
-proof (nominal_induct B rule: ty.induct)
+proof (nominal_induct B rule: ty.strong_induct)
   case (PR X)
   { case 1 show ?case 
       apply -
@@ -12739,7 +12739,7 @@
   assumes a: "<a>:NotR (x).M a \<in> (\<parallel><B>\<parallel>)" "<a>:NotR (x).M a \<notin> BINDINGc B (\<parallel>(B)\<parallel>)"
   shows "\<exists>B'. B = NOT B' \<and> (x):M \<in> (\<parallel>(B')\<parallel>)" 
 using a
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)
 apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
 apply(drule_tac pi="[(a,aa)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
@@ -12750,7 +12750,7 @@
   assumes a: "(x):NotL <a>.M x \<in> NEGn B (\<parallel><B>\<parallel>)" "(x):NotL <a>.M x \<notin> BINDINGn B (\<parallel><B>\<parallel>)"
   shows "\<exists>B'. B = NOT B' \<and> <a>:M \<in> (\<parallel><B'>\<parallel>)" 
 using a
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)
 apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
 apply(drule_tac pi="[(x,xa)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
@@ -12763,7 +12763,7 @@
   assumes a: "<a>:AndR <b>.M <c>.N a \<in> (\<parallel><B>\<parallel>)" "<a>:AndR <b>.M <c>.N a \<notin> BINDINGc B (\<parallel>(B)\<parallel>)"
   shows "\<exists>B1 B2. B = B1 AND B2 \<and> <b>:M \<in> (\<parallel><B1>\<parallel>) \<and> <c>:N \<in> (\<parallel><B2>\<parallel>)" 
 using a
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)
 apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
 apply(drule_tac pi="[(a,ca)]" and x="<a>:Ma" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
@@ -12844,7 +12844,7 @@
   assumes a: "<a>:OrR1 <b>.M a \<in> (\<parallel><B>\<parallel>)" "<a>:OrR1 <b>.M a \<notin> BINDINGc B (\<parallel>(B)\<parallel>)"
   shows "\<exists>B1 B2. B = B1 OR B2 \<and> <b>:M \<in> (\<parallel><B1>\<parallel>)" 
 using a
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)
 apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
 apply(drule_tac pi="[(a,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
@@ -12865,7 +12865,7 @@
   assumes a: "<a>:OrR2 <b>.M a \<in> (\<parallel><B>\<parallel>)" "<a>:OrR2 <b>.M a \<notin> BINDINGc B (\<parallel>(B)\<parallel>)"
   shows "\<exists>B1 B2. B = B1 OR B2 \<and> <b>:M \<in> (\<parallel><B2>\<parallel>)" 
 using a
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)
 apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
 apply(drule_tac pi="[(a,ba)]" in pt_set_bij2[OF pt_coname_inst, OF at_coname_inst])
@@ -12886,7 +12886,7 @@
   assumes a: "(x):(OrL (y).M (z).N x) \<in> NEGn B (\<parallel><B>\<parallel>)" "(x):(OrL (y).M (z).N x) \<notin> BINDINGn B (\<parallel><B>\<parallel>)"
   shows "\<exists>B1 B2. B = B1 OR B2 \<and> (y):M \<in> (\<parallel>(B1)\<parallel>) \<and> (z):N \<in> (\<parallel>(B2)\<parallel>)" 
 using a
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)
 apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
 apply(drule_tac pi="[(x,za)]" and x="(x):Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
@@ -12969,7 +12969,7 @@
   assumes a: "(x):(AndL1 (y).M x) \<in> NEGn B (\<parallel><B>\<parallel>)" "(x):(AndL1 (y).M x) \<notin> BINDINGn B (\<parallel><B>\<parallel>)"
   shows "\<exists>B1 B2. B = B1 AND B2 \<and> (y):M \<in> (\<parallel>(B1)\<parallel>)" 
 using a
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)
 apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
 apply(drule_tac pi="[(x,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
@@ -12992,7 +12992,7 @@
   assumes a: "(x):(AndL2 (y).M x) \<in> NEGn B (\<parallel><B>\<parallel>)" "(x):(AndL2 (y).M x) \<notin> BINDINGn B (\<parallel><B>\<parallel>)"
   shows "\<exists>B1 B2. B = B1 AND B2 \<and> (y):M \<in> (\<parallel>(B2)\<parallel>)" 
 using a
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)
 apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
 apply(drule_tac pi="[(x,ya)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
@@ -13015,7 +13015,7 @@
   assumes a: "(x):(ImpL <a>.M (z).N x) \<in> NEGn B (\<parallel><B>\<parallel>)" "(x):(ImpL <a>.M (z).N x) \<notin> BINDINGn B (\<parallel><B>\<parallel>)"
   shows "\<exists>B1 B2. B = B1 IMP B2 \<and> <a>:M \<in> (\<parallel><B1>\<parallel>) \<and> (z):N \<in> (\<parallel>(B2)\<parallel>)" 
 using a
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(simp_all add: ty.inject AXIOMSn_def ntrm.inject alpha)
 apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm)
 apply(drule_tac pi="[(x,y)]" and x="<aa>:Ma" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
@@ -13052,7 +13052,7 @@
                  (\<forall>z P. x\<sharp>(z,P) \<and> (z):P \<in> \<parallel>(B2)\<parallel> \<longrightarrow> (x):(M{b:=(z).P}) \<in> \<parallel>(B1)\<parallel>) \<and>
                  (\<forall>c Q. b\<sharp>(c,Q) \<and> <c>:Q \<in> \<parallel><B1>\<parallel> \<longrightarrow> <b>:(M{x:=<c>.Q}) \<in> \<parallel><B2>\<parallel>)" 
 using a
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(simp_all add: ty.inject AXIOMSc_def ctrm.inject alpha)
 apply(auto intro: CANDs_alpha simp add: trm.inject calc_atm abs_fresh fresh_atm fresh_prod fresh_bij)
 apply(generate_fresh "name") 
@@ -13457,7 +13457,7 @@
 lemma CANDs_imply_SNa:
   shows "<a>:M \<in> \<parallel><B>\<parallel> \<Longrightarrow> SNa M"
   and   "(x):M \<in> \<parallel>(B)\<parallel> \<Longrightarrow> SNa M"
-proof(induct B arbitrary: a x M rule: ty.weak_induct)
+proof(induct B arbitrary: a x M rule: ty.induct)
   case (PR X)
   { case 1 
     have "<a>:M \<in> \<parallel><PR X>\<parallel>" by fact
@@ -13764,7 +13764,7 @@
 lemma CANDs_preserved:
   shows "<a>:M \<in> \<parallel><B>\<parallel> \<Longrightarrow> M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> <a>:M' \<in> \<parallel><B>\<parallel>"
   and   "(x):M \<in> \<parallel>(B)\<parallel> \<Longrightarrow> M \<longrightarrow>\<^isub>a* M' \<Longrightarrow> (x):M' \<in> \<parallel>(B)\<parallel>" 
-proof(nominal_induct B arbitrary: a x M M' rule: ty.induct) 
+proof(nominal_induct B arbitrary: a x M M' rule: ty.strong_induct) 
   case (PR X)
   { case 1 
     have asm: "M \<longrightarrow>\<^isub>a* M'" by fact
@@ -14135,7 +14135,7 @@
   and     b: "<a>:M \<in> \<parallel><B>\<parallel>"
   shows "<a>:M \<in> AXIOMSc B \<or> <a>:M \<in> BINDINGc B (\<parallel>(B)\<parallel>)"
 using a b
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(simp)
 apply(simp)
 apply(erule disjE)
@@ -14202,7 +14202,7 @@
   and     b: "(x):M \<in> (NEGn B (\<parallel><B>\<parallel>))"
   shows "(x):M \<in> AXIOMSn B \<or> (x):M \<in> BINDINGn B (\<parallel><B>\<parallel>)"
 using a b
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(simp)
 apply(simp)
 apply(erule disjE)
@@ -14278,10 +14278,10 @@
   shows "<c>:M \<in> BINDINGc B (\<parallel>(B)\<parallel>) \<Longrightarrow> <c>:M \<in> (\<parallel><B>\<parallel>)"
   and   "(x):N \<in> BINDINGn B (\<parallel><B>\<parallel>) \<Longrightarrow> (x):N \<in> (\<parallel>(B)\<parallel>)"
 apply -
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(auto)
 apply(rule NEG_intro)
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(auto)
 done
 
@@ -14344,7 +14344,7 @@
   assumes a: "fic M c" "c\<sharp>(a,b)"
   shows "fic (M[a\<turnstile>c>b]) c" 
 using a
-apply(nominal_induct M avoiding: c a b rule: trm.induct)
+apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
 apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
 done
 
@@ -14359,7 +14359,7 @@
   assumes a: "fin M y"
   shows "fin (M[a\<turnstile>c>b]) y" 
 using a
-apply(nominal_induct M avoiding: a b rule: trm.induct)
+apply(nominal_induct M avoiding: a b rule: trm.strong_induct)
 apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
 done
 
@@ -14375,7 +14375,7 @@
   assumes a: "c\<sharp>(M[a\<turnstile>c>b])" "c\<sharp>(a,b)"
   shows "c\<sharp>M"
 using a
-apply(nominal_induct M avoiding: c a b rule: trm.induct)
+apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
 apply(auto split: if_splits simp add: abs_fresh)
 done
 
@@ -14384,7 +14384,7 @@
   assumes a: "x\<sharp>(M[a\<turnstile>c>b])" 
   shows "x\<sharp>M"
 using a
-apply(nominal_induct M avoiding: x a b rule: trm.induct)
+apply(nominal_induct M avoiding: x a b rule: trm.strong_induct)
 apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp fresh_atm)
 done
 
@@ -14393,7 +14393,7 @@
   assumes a: "fic (M[a\<turnstile>c>b]) c" "c\<sharp>(a,b)"
   shows "fic M c" 
 using a
-apply(nominal_induct M avoiding: c a b rule: trm.induct)
+apply(nominal_induct M avoiding: c a b rule: trm.strong_induct)
 apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
            split: if_splits)
 apply(auto dest: crename_fresh_interesting1 simp add: fresh_prod fresh_atm)
@@ -14403,7 +14403,7 @@
   assumes a: "fin (M[a\<turnstile>c>b]) x"
   shows "fin M x" 
 using a
-apply(nominal_induct M avoiding: x a b rule: trm.induct)
+apply(nominal_induct M avoiding: x a b rule: trm.strong_induct)
 apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
            split: if_splits)
 apply(auto dest: crename_fresh_interesting2 simp add: fresh_prod fresh_atm)
@@ -14413,7 +14413,7 @@
   assumes a: "R[a\<turnstile>c>b] = Cut <c>.M (x).N" "c\<sharp>(a,b,N,R)" "x\<sharp>(M,R)"
   shows "\<exists>M' N'. R = Cut <c>.M' (x).N' \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> x\<sharp>M'"
 using a
-apply(nominal_induct R avoiding: a b c x M N rule: trm.induct)
+apply(nominal_induct R avoiding: a b c x M N rule: trm.strong_induct)
 apply(auto split: if_splits)
 apply(simp add: trm.inject)
 apply(auto simp add: alpha)
@@ -14452,7 +14452,7 @@
   assumes a: "R[a\<turnstile>c>b] = NotR (x).N c" "x\<sharp>R" "c\<sharp>(a,b)"
   shows "\<exists>N'. (R = NotR (x).N' c) \<and> N'[a\<turnstile>c>b] = N" 
 using a
-apply(nominal_induct R avoiding: a b c x N rule: trm.induct)
+apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(name,x)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -14466,7 +14466,7 @@
   assumes a: "R[a\<turnstile>c>b] = NotR (x).N c" "x\<sharp>R" "c\<sharp>a"
   shows "(\<exists>N'. (R = NotR (x).N' c) \<and> N'[a\<turnstile>c>b] = N) \<or> (\<exists>N'. (R = NotR (x).N' a) \<and> b=c \<and> N'[a\<turnstile>c>b] = N)"
 using a
-apply(nominal_induct R avoiding: a b c x N rule: trm.induct)
+apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
 apply(rule_tac x="[(name,x)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -14486,7 +14486,7 @@
   assumes a: "R[a\<turnstile>c>b] = NotR (x).N c" 
   shows "(a=c \<and> a=b) \<or> (a\<noteq>c)" 
 using a
-apply(nominal_induct R avoiding: a b c x N rule: trm.induct)
+apply(nominal_induct R avoiding: a b c x N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 done
 
@@ -14494,7 +14494,7 @@
   assumes a: "R[a\<turnstile>c>b] = NotL <c>.N y" "c\<sharp>(R,a,b)"
   shows "\<exists>N'. (R = NotL <c>.N' y) \<and> N'[a\<turnstile>c>b] = N" 
 using a
-apply(nominal_induct R avoiding: a b c y N rule: trm.induct)
+apply(nominal_induct R avoiding: a b c y N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(coname,c)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -14508,7 +14508,7 @@
   assumes a: "R[a\<turnstile>c>b] = AndL1 (x).N y" "x\<sharp>R"
   shows "\<exists>N'. (R = AndL1 (x).N' y) \<and> N'[a\<turnstile>c>b] = N" 
 using a
-apply(nominal_induct R avoiding: a b x y N rule: trm.induct)
+apply(nominal_induct R avoiding: a b x y N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(name1,x)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -14522,7 +14522,7 @@
   assumes a: "R[a\<turnstile>c>b] = AndL2 (x).N y" "x\<sharp>R"
   shows "\<exists>N'. (R = AndL2 (x).N' y) \<and> N'[a\<turnstile>c>b] = N" 
 using a
-apply(nominal_induct R avoiding: a b x y N rule: trm.induct)
+apply(nominal_induct R avoiding: a b x y N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(name1,x)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -14536,7 +14536,7 @@
   assumes a: "R[a\<turnstile>c>b] = AndR <c>.M <d>.N e" 
   shows "(a=e \<and> a=b) \<or> (a\<noteq>e)" 
 using a
-apply(nominal_induct R avoiding: a b c d e M N rule: trm.induct)
+apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 done
 
@@ -14544,7 +14544,7 @@
   assumes a: "R[a\<turnstile>c>b] = AndR <c>.M <d>.N e" "c\<sharp>(a,b,d,e,N,R)" "d\<sharp>(a,b,c,e,M,R)" "e\<sharp>(a,b)"
   shows "\<exists>M' N'. R = AndR <c>.M' <d>.N' e \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> d\<sharp>M'"
 using a
-apply(nominal_induct R avoiding: a b c d e M N rule: trm.induct)
+apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: trm.inject alpha)
 apply(simp add: fresh_atm fresh_prod)
 apply(rule_tac x="[(coname2,d)]\<bullet>trm2" in exI)
@@ -14581,7 +14581,7 @@
   shows "(\<exists>M' N'. R = AndR <c>.M' <d>.N' e \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> d\<sharp>M') \<or>
          (\<exists>M' N'. R = AndR <c>.M' <d>.N' a \<and> b=e \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> d\<sharp>M')"
 using a
-apply(nominal_induct R avoiding: a b c d e M N rule: trm.induct)
+apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: trm.inject alpha)[1]
 apply(auto split: if_splits simp add: trm.inject alpha)[1]
 apply(auto split: if_splits simp add: trm.inject alpha)[1]
@@ -14621,7 +14621,7 @@
   assumes a: "R[a\<turnstile>c>b] = OrR1 <c>.M e" 
   shows "(a=e \<and> a=b) \<or> (a\<noteq>e)" 
 using a
-apply(nominal_induct R avoiding: a b c e M rule: trm.induct)
+apply(nominal_induct R avoiding: a b c e M rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 done
 
@@ -14629,7 +14629,7 @@
   assumes a: "R[a\<turnstile>c>b] = OrR1 <c>.N d" "c\<sharp>(R,a,b)" "d\<sharp>(a,b)"
   shows "\<exists>N'. (R = OrR1 <c>.N' d) \<and> N'[a\<turnstile>c>b] = N" 
 using a
-apply(nominal_induct R avoiding: a b c d N rule: trm.induct)
+apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(coname1,c)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -14644,7 +14644,7 @@
   shows "(\<exists>N'. (R = OrR1 <c>.N' d) \<and> N'[a\<turnstile>c>b] = N) \<or>
          (\<exists>N'. (R = OrR1 <c>.N' a) \<and> b=d \<and> N'[a\<turnstile>c>b] = N)" 
 using a
-apply(nominal_induct R avoiding: a b c d N rule: trm.induct)
+apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(coname1,c)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -14664,7 +14664,7 @@
   assumes a: "R[a\<turnstile>c>b] = OrR2 <c>.M e" 
   shows "(a=e \<and> a=b) \<or> (a\<noteq>e)" 
 using a
-apply(nominal_induct R avoiding: a b c e M rule: trm.induct)
+apply(nominal_induct R avoiding: a b c e M rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 done
 
@@ -14672,7 +14672,7 @@
   assumes a: "R[a\<turnstile>c>b] = OrR2 <c>.N d" "c\<sharp>(R,a,b)" "d\<sharp>(a,b)"
   shows "\<exists>N'. (R = OrR2 <c>.N' d) \<and> N'[a\<turnstile>c>b] = N" 
 using a
-apply(nominal_induct R avoiding: a b c d N rule: trm.induct)
+apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(coname1,c)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -14687,7 +14687,7 @@
   shows "(\<exists>N'. (R = OrR2 <c>.N' d) \<and> N'[a\<turnstile>c>b] = N) \<or>
          (\<exists>N'. (R = OrR2 <c>.N' a) \<and> b=d \<and> N'[a\<turnstile>c>b] = N)" 
 using a
-apply(nominal_induct R avoiding: a b c d N rule: trm.induct)
+apply(nominal_induct R avoiding: a b c d N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(coname1,c)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -14707,7 +14707,7 @@
   assumes a: "R[a\<turnstile>c>b] = OrL (x).M (y).N z" "x\<sharp>(y,z,N,R)" "y\<sharp>(x,z,M,R)"
   shows "\<exists>M' N'. R = OrL (x).M' (y).N' z \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> x\<sharp>N' \<and> y\<sharp>M'"
 using a
-apply(nominal_induct R avoiding: a b x y z M N rule: trm.induct)
+apply(nominal_induct R avoiding: a b x y z M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: trm.inject alpha)
 apply(rule_tac x="[(name2,y)]\<bullet>trm2" in exI)
 apply(perm_simp)
@@ -14733,7 +14733,7 @@
   assumes a: "R[a\<turnstile>c>b] = ImpL <c>.M (y).N z" "c\<sharp>(a,b,N,R)" "y\<sharp>(z,M,R)"
   shows "\<exists>M' N'. R = ImpL <c>.M' (y).N' z \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> y\<sharp>M'"
 using a
-apply(nominal_induct R avoiding: a b c y z M N rule: trm.induct)
+apply(nominal_induct R avoiding: a b c y z M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: trm.inject alpha)
 apply(rule_tac x="[(name1,y)]\<bullet>trm2" in exI)
 apply(perm_simp)
@@ -14759,7 +14759,7 @@
   assumes a: "R[a\<turnstile>c>b] = ImpR (x).<c>.M e" 
   shows "(a=e \<and> a=b) \<or> (a\<noteq>e)" 
 using a
-apply(nominal_induct R avoiding: x a b c e M rule: trm.induct)
+apply(nominal_induct R avoiding: x a b c e M rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 done
 
@@ -14767,7 +14767,7 @@
   assumes a: "R[a\<turnstile>c>b] = ImpR (x).<c>.N d" "c\<sharp>(R,a,b)" "d\<sharp>(a,b)" "x\<sharp>R" 
   shows "\<exists>N'. (R = ImpR (x).<c>.N' d) \<and> N'[a\<turnstile>c>b] = N" 
 using a
-apply(nominal_induct R avoiding: a b x c d N rule: trm.induct)
+apply(nominal_induct R avoiding: a b x c d N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_perm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(name,x)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -14787,7 +14787,7 @@
   shows "(\<exists>N'. (R = ImpR (x).<c>.N' d) \<and> N'[a\<turnstile>c>b] = N) \<or>
          (\<exists>N'. (R = ImpR (x).<c>.N' a) \<and> b=d \<and> N'[a\<turnstile>c>b] = N)" 
 using a
-apply(nominal_induct R avoiding: x a b c d N rule: trm.induct)
+apply(nominal_induct R avoiding: x a b c d N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject abs_perm calc_atm)
 apply(rule_tac x="[(name,x)]\<bullet>[(coname1,c)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -14809,7 +14809,7 @@
   assumes a: "N[a\<turnstile>c>b] = Ax x c"
   shows "\<exists>d. N = Ax x d"
 using a
-apply(nominal_induct N avoiding: a b rule: trm.induct)
+apply(nominal_induct N avoiding: a b rule: trm.strong_induct)
 apply(auto split: if_splits)
 apply(simp add: trm.inject)
 done
@@ -14818,7 +14818,7 @@
   assumes a: "distinct [a,b,c]"
   shows "M[a\<turnstile>c>c][c\<turnstile>c>b] = M[c\<turnstile>c>b][a\<turnstile>c>b]"
 using a
-apply(nominal_induct M avoiding: a c b rule: trm.induct)
+apply(nominal_induct M avoiding: a c b rule: trm.strong_induct)
 apply(auto simp add: rename_fresh simp add: trm.inject alpha)
 apply(blast)
 apply(rotate_tac 12)
@@ -14836,13 +14836,13 @@
   assumes a: "a\<noteq>c" "a\<noteq>d" "a\<noteq>b" "c\<noteq>d" "b\<noteq>c"
   shows "M[a\<turnstile>c>b][c\<turnstile>c>d] = M[c\<turnstile>c>d][a\<turnstile>c>b]"
 using a
-apply(nominal_induct M avoiding: a c b d rule: trm.induct)
+apply(nominal_induct M avoiding: a c b d rule: trm.strong_induct)
 apply(auto simp add: rename_fresh simp add: trm.inject alpha)
 done
 
 lemma crename_interesting3:
   shows "M[a\<turnstile>c>c][x\<turnstile>n>y] = M[x\<turnstile>n>y][a\<turnstile>c>c]"
-apply(nominal_induct M avoiding: a c x y rule: trm.induct)
+apply(nominal_induct M avoiding: a c x y rule: trm.strong_induct)
 apply(auto simp add: rename_fresh simp add: trm.inject alpha)
 done
 
@@ -15452,7 +15452,7 @@
   assumes a: "distinct [x,y,z]"
   shows "M[x\<turnstile>n>z][z\<turnstile>n>y] = M[z\<turnstile>n>y][x\<turnstile>n>y]"
 using a
-apply(nominal_induct M avoiding: x y z rule: trm.induct)
+apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
 apply(auto simp add: rename_fresh simp add: trm.inject alpha)
 apply(blast)
 apply(blast)
@@ -15476,7 +15476,7 @@
   assumes a: "x\<noteq>z" "x\<noteq>u" "x\<noteq>y" "z\<noteq>u" "y\<noteq>z"
   shows "M[x\<turnstile>n>y][z\<turnstile>n>u] = M[z\<turnstile>n>u][x\<turnstile>n>y]"
 using a
-apply(nominal_induct M avoiding: x y z u rule: trm.induct)
+apply(nominal_induct M avoiding: x y z u rule: trm.strong_induct)
 apply(auto simp add: rename_fresh simp add: trm.inject alpha)
 done
 
@@ -15484,7 +15484,7 @@
   assumes a: "fic M c" 
   shows "fic (M[x\<turnstile>n>y]) c" 
 using a
-apply(nominal_induct M avoiding: c x y rule: trm.induct)
+apply(nominal_induct M avoiding: c x y rule: trm.strong_induct)
 apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh)
 done
 
@@ -15499,7 +15499,7 @@
   assumes a: "fin M z" "z\<sharp>(x,y)"
   shows "fin (M[x\<turnstile>n>y]) z" 
 using a
-apply(nominal_induct M avoiding: x y z rule: trm.induct)
+apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
 apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
            split: if_splits)
 done
@@ -15509,7 +15509,7 @@
   assumes a: "z\<sharp>(M[x\<turnstile>n>y])" "z\<sharp>(x,y)"
   shows "z\<sharp>M"
 using a
-apply(nominal_induct M avoiding: x y z rule: trm.induct)
+apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
 apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp)
 done
 
@@ -15518,7 +15518,7 @@
   assumes a: "c\<sharp>(M[x\<turnstile>n>y])" 
   shows "c\<sharp>M"
 using a
-apply(nominal_induct M avoiding: x y c rule: trm.induct)
+apply(nominal_induct M avoiding: x y c rule: trm.strong_induct)
 apply(auto split: if_splits simp add: abs_fresh abs_supp fin_supp fresh_atm)
 done
 
@@ -15526,7 +15526,7 @@
   assumes a: "fin (M[x\<turnstile>n>y]) z" "z\<sharp>(x,y)"
   shows "fin M z" 
 using a
-apply(nominal_induct M avoiding: x y z rule: trm.induct)
+apply(nominal_induct M avoiding: x y z rule: trm.strong_induct)
 apply(auto dest!: fin_elims intro!: fin.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
            split: if_splits)
 apply(auto dest: nrename_fresh_interesting1 simp add: fresh_atm fresh_prod)
@@ -15536,7 +15536,7 @@
   assumes a: "R[x\<turnstile>n>y] = Cut <c>.M (z).N" "c\<sharp>(N,R)" "z\<sharp>(x,y,M,R)"
   shows "\<exists>M' N'. R = Cut <c>.M' (z).N' \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N \<and> c\<sharp>N' \<and> z\<sharp>M'"
 using a
-apply(nominal_induct R avoiding: c y x z M N rule: trm.induct)
+apply(nominal_induct R avoiding: c y x z M N rule: trm.strong_induct)
 apply(auto split: if_splits)
 apply(simp add: trm.inject)
 apply(auto simp add: alpha fresh_atm)
@@ -15561,7 +15561,7 @@
   assumes a: "R[x\<turnstile>n>y] = NotR (z).N c" "z\<sharp>(R,x,y)" 
   shows "\<exists>N'. (R = NotR (z).N' c) \<and> N'[x\<turnstile>n>y] = N" 
 using a
-apply(nominal_induct R avoiding: x y c z N rule: trm.induct)
+apply(nominal_induct R avoiding: x y c z N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(name,z)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -15575,7 +15575,7 @@
   assumes a: "R[x\<turnstile>n>y] = NotL <c>.N z" "c\<sharp>R" "z\<sharp>(x,y)"
   shows "\<exists>N'. (R = NotL <c>.N' z) \<and> N'[x\<turnstile>n>y] = N" 
 using a
-apply(nominal_induct R avoiding: x y c z N rule: trm.induct)
+apply(nominal_induct R avoiding: x y c z N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(coname,c)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -15589,7 +15589,7 @@
   assumes a: "R[x\<turnstile>n>y] = NotL <c>.N u" "c\<sharp>R" "x\<noteq>y" 
   shows "(\<exists>N'. (R = NotL <c>.N' u) \<and> N'[x\<turnstile>n>y] = N) \<or> (\<exists>N'. (R = NotL <c>.N' x) \<and> y=u \<and> N'[x\<turnstile>n>y] = N)"
 using a
-apply(nominal_induct R avoiding: y u c x N rule: trm.induct)
+apply(nominal_induct R avoiding: y u c x N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
 apply(rule_tac x="[(coname,c)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -15609,7 +15609,7 @@
   assumes a: "R[x\<turnstile>n>y] = NotL <c>.N u" 
   shows "(x=u \<and> x=y) \<or> (x\<noteq>u)" 
 using a
-apply(nominal_induct R avoiding: y u c x N rule: trm.induct)
+apply(nominal_induct R avoiding: y u c x N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 done
 
@@ -15617,7 +15617,7 @@
   assumes a: "R[x\<turnstile>n>y] = AndL1 (z).N u" "z\<sharp>(R,x,y)" "u\<sharp>(x,y)"
   shows "\<exists>N'. (R = AndL1 (z).N' u) \<and> N'[x\<turnstile>n>y] = N" 
 using a
-apply(nominal_induct R avoiding: z u x y N rule: trm.induct)
+apply(nominal_induct R avoiding: z u x y N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(name1,z)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -15631,7 +15631,7 @@
   assumes a: "R[x\<turnstile>n>y] = AndL1 (v).N u" "v\<sharp>(R,u,x,y)" "x\<noteq>y" 
   shows "(\<exists>N'. (R = AndL1 (v).N' u) \<and> N'[x\<turnstile>n>y] = N) \<or> (\<exists>N'. (R = AndL1 (v).N' x) \<and> y=u \<and> N'[x\<turnstile>n>y] = N)"
 using a
-apply(nominal_induct R avoiding: y u v x N rule: trm.induct)
+apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
 apply(rule_tac x="[(name1,v)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -15651,7 +15651,7 @@
   assumes a: "R[x\<turnstile>n>y] = AndL1 (v).N u" 
   shows "(x=u \<and> x=y) \<or> (x\<noteq>u)" 
 using a
-apply(nominal_induct R avoiding: y u v x N rule: trm.induct)
+apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 done
 
@@ -15659,7 +15659,7 @@
   assumes a: "R[x\<turnstile>n>y] = AndL2 (z).N u" "z\<sharp>(R,x,y)" "u\<sharp>(x,y)"
   shows "\<exists>N'. (R = AndL2 (z).N' u) \<and> N'[x\<turnstile>n>y] = N" 
 using a
-apply(nominal_induct R avoiding: z u x y N rule: trm.induct)
+apply(nominal_induct R avoiding: z u x y N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(name1,z)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -15673,7 +15673,7 @@
   assumes a: "R[x\<turnstile>n>y] = AndL2 (v).N u" "v\<sharp>(R,u,x,y)" "x\<noteq>y" 
   shows "(\<exists>N'. (R = AndL2 (v).N' u) \<and> N'[x\<turnstile>n>y] = N) \<or> (\<exists>N'. (R = AndL2 (v).N' x) \<and> y=u \<and> N'[x\<turnstile>n>y] = N)"
 using a
-apply(nominal_induct R avoiding: y u v x N rule: trm.induct)
+apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
 apply(rule_tac x="[(name1,v)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -15693,7 +15693,7 @@
   assumes a: "R[x\<turnstile>n>y] = AndL2 (v).N u" 
   shows "(x=u \<and> x=y) \<or> (x\<noteq>u)" 
 using a
-apply(nominal_induct R avoiding: y u v x N rule: trm.induct)
+apply(nominal_induct R avoiding: y u v x N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 done
 
@@ -15701,7 +15701,7 @@
   assumes a: "R[x\<turnstile>n>y] = AndR <c>.M <d>.N e" "c\<sharp>(d,e,N,R)" "d\<sharp>(c,e,M,R)" 
   shows "\<exists>M' N'. R = AndR <c>.M' <d>.N' e \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N \<and> c\<sharp>N' \<and> d\<sharp>M'"
 using a
-apply(nominal_induct R avoiding: x y c d e M N rule: trm.induct)
+apply(nominal_induct R avoiding: x y c d e M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: trm.inject alpha)
 apply(simp add: fresh_atm fresh_prod)
 apply(rule_tac x="[(coname1,c)]\<bullet>trm1" in exI)
@@ -15725,7 +15725,7 @@
   assumes a: "R[x\<turnstile>n>y] = OrR1 <c>.N d" "c\<sharp>(R,d)" 
   shows "\<exists>N'. (R = OrR1 <c>.N' d) \<and> N'[x\<turnstile>n>y] = N" 
 using a
-apply(nominal_induct R avoiding: x y c d N rule: trm.induct)
+apply(nominal_induct R avoiding: x y c d N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(coname1,c)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -15739,7 +15739,7 @@
   assumes a: "R[x\<turnstile>n>y] = OrR2 <c>.N d" "c\<sharp>(R,d)" 
   shows "\<exists>N'. (R = OrR2 <c>.N' d) \<and> N'[x\<turnstile>n>y] = N" 
 using a
-apply(nominal_induct R avoiding: x y c d N rule: trm.induct)
+apply(nominal_induct R avoiding: x y c d N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(coname1,c)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -15753,7 +15753,7 @@
   assumes a: "R[u\<turnstile>n>v] = OrL (x).M (y).N z" "x\<sharp>(y,z,u,v,N,R)" "y\<sharp>(x,z,u,v,M,R)" "z\<sharp>(u,v)"
   shows "\<exists>M' N'. R = OrL (x).M' (y).N' z \<and> M'[u\<turnstile>n>v] = M \<and> N'[u\<turnstile>n>v] = N \<and> x\<sharp>N' \<and> y\<sharp>M'"
 using a
-apply(nominal_induct R avoiding: u v x y z M N rule: trm.induct)
+apply(nominal_induct R avoiding: u v x y z M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: trm.inject alpha fresh_prod fresh_atm)
 apply(rule_tac x="[(name1,x)]\<bullet>trm1" in exI)
 apply(perm_simp)
@@ -15774,7 +15774,7 @@
   shows "(\<exists>M' N'. (R = OrL (v).M' (w).N' u) \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N) \<or> 
          (\<exists>M' N'. (R = OrL (v).M' (w).N' x) \<and> y=u \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N)"
 using a
-apply(nominal_induct R avoiding: y x u v w M N rule: trm.induct)
+apply(nominal_induct R avoiding: y x u v w M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
 apply(rule_tac x="[(name1,v)]\<bullet>trm1" in exI)
 apply(perm_simp)
@@ -15808,7 +15808,7 @@
   assumes a: "R[x\<turnstile>n>y] = OrL (v).M (w).N u" 
   shows "(x=u \<and> x=y) \<or> (x\<noteq>u)" 
 using a
-apply(nominal_induct R avoiding: y x w u v M N rule: trm.induct)
+apply(nominal_induct R avoiding: y x w u v M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 done
 
@@ -15816,7 +15816,7 @@
   assumes a: "R[x\<turnstile>n>y] = ImpL <c>.M (u).N z" "c\<sharp>(N,R)" "u\<sharp>(y,x,z,M,R)" "z\<sharp>(x,y)"
   shows "\<exists>M' N'. R = ImpL <c>.M' (u).N' z \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N \<and> c\<sharp>N' \<and> u\<sharp>M'"
 using a
-apply(nominal_induct R avoiding: u x c y z M N rule: trm.induct)
+apply(nominal_induct R avoiding: u x c y z M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: trm.inject alpha fresh_prod fresh_atm)
 apply(rule_tac x="[(coname,c)]\<bullet>trm1" in exI)
 apply(perm_simp)
@@ -15837,7 +15837,7 @@
   shows "(\<exists>M' N'. (R = ImpL <c>.M' (w).N' u) \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N) \<or> 
          (\<exists>M' N'. (R = ImpL <c>.M' (w).N' x) \<and> y=u \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N)"
 using a
-apply(nominal_induct R avoiding: y x u c w M N rule: trm.induct)
+apply(nominal_induct R avoiding: y x u c w M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
 apply(rule_tac x="[(coname,c)]\<bullet>trm1" in exI)
 apply(perm_simp)
@@ -15871,7 +15871,7 @@
   assumes a: "R[x\<turnstile>n>y] = ImpL <c>.M (w).N u" 
   shows "(x=u \<and> x=y) \<or> (x\<noteq>u)" 
 using a
-apply(nominal_induct R avoiding: y x w u c M N rule: trm.induct)
+apply(nominal_induct R avoiding: y x w u c M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm alpha abs_fresh trm.inject)
 done
 
@@ -15879,7 +15879,7 @@
   assumes a: "R[u\<turnstile>n>v] = ImpR (x).<c>.N d" "c\<sharp>(R,d)" "x\<sharp>(R,u,v)" 
   shows "\<exists>N'. (R = ImpR (x).<c>.N' d) \<and> N'[u\<turnstile>n>v] = N" 
 using a
-apply(nominal_induct R avoiding: u v x c d N rule: trm.induct)
+apply(nominal_induct R avoiding: u v x c d N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_perm alpha abs_fresh trm.inject)
 apply(rule_tac x="[(name,x)]\<bullet>trm" in exI)
 apply(perm_simp)
@@ -15929,7 +15929,7 @@
   assumes a: "N[x\<turnstile>n>y] = Ax z c"
   shows "\<exists>z. N = Ax z c"
 using a
-apply(nominal_induct N avoiding: x y rule: trm.induct)
+apply(nominal_induct N avoiding: x y rule: trm.strong_induct)
 apply(auto split: if_splits)
 apply(simp add: trm.inject)
 done
@@ -15938,7 +15938,7 @@
   assumes a: "fic (M[x\<turnstile>n>y]) c" 
   shows "fic M c" 
 using a
-apply(nominal_induct M avoiding: c x y rule: trm.induct)
+apply(nominal_induct M avoiding: c x y rule: trm.strong_induct)
 apply(auto dest!: fic_elims intro!: fic.intros simp add: fresh_prod fresh_atm rename_fresh abs_fresh
            split: if_splits)
 apply(auto dest: nrename_fresh_interesting2 simp add: fresh_prod fresh_atm)
@@ -17865,9 +17865,9 @@
   shows "(pi1\<bullet>(stn M \<theta>n)) = stn (pi1\<bullet>M) (pi1\<bullet>\<theta>n)"
   and   "(pi2\<bullet>(stn M \<theta>n)) = stn (pi2\<bullet>M) (pi2\<bullet>\<theta>n)"
 apply -
-apply(nominal_induct M avoiding: \<theta>n rule: trm.induct)
+apply(nominal_induct M avoiding: \<theta>n rule: trm.strong_induct)
 apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm)
-apply(nominal_induct M avoiding: \<theta>n rule: trm.induct)
+apply(nominal_induct M avoiding: \<theta>n rule: trm.strong_induct)
 apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm)
 done
 
@@ -17877,9 +17877,9 @@
   shows "(pi1\<bullet>(stc M \<theta>c)) = stc (pi1\<bullet>M) (pi1\<bullet>\<theta>c)"
   and   "(pi2\<bullet>(stc M \<theta>c)) = stc (pi2\<bullet>M) (pi2\<bullet>\<theta>c)"
 apply -
-apply(nominal_induct M avoiding: \<theta>c rule: trm.induct)
+apply(nominal_induct M avoiding: \<theta>c rule: trm.strong_induct)
 apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm)
-apply(nominal_induct M avoiding: \<theta>c rule: trm.induct)
+apply(nominal_induct M avoiding: \<theta>c rule: trm.strong_induct)
 apply(auto simp add: eqvts fresh_bij fresh_prod eq_bij fresh_atm)
 done
 
@@ -17888,7 +17888,7 @@
   and   x::"name"
   shows "a\<sharp>(\<theta>n,M) \<Longrightarrow> a\<sharp>stn M \<theta>n"
   and   "x\<sharp>(\<theta>n,M) \<Longrightarrow> x\<sharp>stn M \<theta>n"
-apply(nominal_induct M avoiding: \<theta>n a x rule: trm.induct)
+apply(nominal_induct M avoiding: \<theta>n a x rule: trm.strong_induct)
 apply(auto simp add: abs_fresh fresh_prod fresh_atm)
 apply(rule lookupc_freshness)
 apply(simp add: fresh_atm)
@@ -17901,7 +17901,7 @@
   and   x::"name"
   shows "a\<sharp>(\<theta>c,M) \<Longrightarrow> a\<sharp>stc M \<theta>c"
   and   "x\<sharp>(\<theta>c,M) \<Longrightarrow> x\<sharp>stc M \<theta>c"
-apply(nominal_induct M avoiding: \<theta>c a x rule: trm.induct)
+apply(nominal_induct M avoiding: \<theta>c a x rule: trm.strong_induct)
 apply(auto simp add: abs_fresh fresh_prod fresh_atm)
 apply(rule lookupd_freshness)
 apply(simp add: fresh_atm)
@@ -18128,7 +18128,7 @@
   and   pi2::"coname prm"
   shows "pi1\<bullet>(\<theta>n,\<theta>c<M>) = (pi1\<bullet>\<theta>n),(pi1\<bullet>\<theta>c)<(pi1\<bullet>M)>"
   and   "pi2\<bullet>(\<theta>n,\<theta>c<M>) = (pi2\<bullet>\<theta>n),(pi2\<bullet>\<theta>c)<(pi2\<bullet>M)>"
-apply(nominal_induct M avoiding: \<theta>n \<theta>c rule: trm.induct)
+apply(nominal_induct M avoiding: \<theta>n \<theta>c rule: trm.strong_induct)
 apply(auto simp add: eq_bij fresh_bij eqvts perm_pi_simp)
 apply(rule case_cong)
 apply(rule find_maps)
@@ -18217,7 +18217,7 @@
   and     b: "a\<sharp>(\<theta>n,\<theta>c)" "x\<sharp>(\<theta>n,\<theta>c)"
   shows "M = Ax x a"
 using a b
-apply(nominal_induct M avoiding: \<theta>n \<theta>c rule: trm.induct)
+apply(nominal_induct M avoiding: \<theta>n \<theta>c rule: trm.strong_induct)
 apply(auto)
 apply(drule lookup_unicity)
 apply(simp)+
@@ -18408,7 +18408,7 @@
   assumes a: "x\<sharp>\<theta>n" "x\<sharp>\<theta>c" "x\<sharp>M"
   shows "x\<sharp>\<theta>n,\<theta>c<M>"
 using a
-apply(nominal_induct M avoiding: x \<theta>n \<theta>c rule: trm.induct)
+apply(nominal_induct M avoiding: x \<theta>n \<theta>c rule: trm.strong_induct)
 apply(simp add: lookup_freshness)
 apply(auto simp add: abs_fresh)[1]
 apply(simp add: lookupc_freshness)
@@ -18494,7 +18494,7 @@
   assumes a: "a\<sharp>\<theta>n" "a\<sharp>\<theta>c" "a\<sharp>M"
   shows "a\<sharp>\<theta>n,\<theta>c<M>"
 using a
-apply(nominal_induct M avoiding: a \<theta>n \<theta>c rule: trm.induct)
+apply(nominal_induct M avoiding: a \<theta>n \<theta>c rule: trm.strong_induct)
 apply(simp add: lookup_freshness)
 apply(auto simp add: abs_fresh)[1]
 apply(simp add: lookupd_freshness)
@@ -18579,7 +18579,7 @@
   assumes a: "a\<sharp>(\<theta>n,\<theta>c)"
   shows "\<theta>n,((a,x,P)#\<theta>c)<M> = ((\<theta>n,\<theta>c<M>){a:=(x).P})"
 using a
-apply(nominal_induct M avoiding: a x \<theta>n \<theta>c P rule: trm.induct)
+apply(nominal_induct M avoiding: a x \<theta>n \<theta>c P rule: trm.strong_induct)
 apply(auto simp add: fresh_list_cons fresh_prod)[1]
 apply(simp add: lookup_csubst)
 apply(simp add: fresh_list_cons fresh_prod)
@@ -18866,7 +18866,7 @@
   assumes a: "x\<sharp>(\<theta>n,\<theta>c)"
   shows "((x,a,P)#\<theta>n),\<theta>c<M> = ((\<theta>n,\<theta>c<M>){x:=<a>.P})"
 using a
-apply(nominal_induct M avoiding: a x \<theta>n \<theta>c P rule: trm.induct)
+apply(nominal_induct M avoiding: a x \<theta>n \<theta>c P rule: trm.strong_induct)
 apply(auto simp add: fresh_list_cons fresh_prod)[1]
 apply(simp add: lookup_fresh)
 apply(rule lookupb_lookupa)
@@ -19337,7 +19337,7 @@
   and   pi2::"coname prm"
   and   B::"ty"
   shows "pi1\<bullet>B=B" and "pi2\<bullet>B=B"
-apply(nominal_induct B rule: ty.induct)
+apply(nominal_induct B rule: ty.strong_induct)
 apply(auto simp add: perm_string)
 done
 
@@ -20394,7 +20394,7 @@
 
 lemma id_redu:
   shows "(idn \<Gamma> x),(idc \<Delta> a)<M> \<longrightarrow>\<^isub>a* M"
-apply(nominal_induct M avoiding: \<Gamma> \<Delta> x a rule: trm.induct)
+apply(nominal_induct M avoiding: \<Gamma> \<Delta> x a rule: trm.strong_induct)
 apply(auto)
 (* Ax *)
 apply(case_tac "name\<sharp>(idn \<Gamma> x)")
diff -r 003b5781b845 -r 071f40487734 src/HOL/Nominal/Examples/Compile.thy
--- a/src/HOL/Nominal/Examples/Compile.thy	Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/Compile.thy	Thu May 22 16:34:41 2008 +0200
@@ -137,7 +137,7 @@
   and   t2::"trmI"
   and   x::"name"
   shows "pi\<bullet>(t1[x::=t2]) = ((pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)])"
-  apply (nominal_induct t1 avoiding: x t2 rule: trmI.induct)
+  apply (nominal_induct t1 avoiding: x t2 rule: trmI.strong_induct)
   apply (simp_all add: Isubst.simps eqvts fresh_bij)
   done
 
@@ -146,7 +146,7 @@
   and   t2::"trmI"
   and   x::"name"
   shows "((supp (t1[x::=t2]))::name set) \<subseteq> (supp t2)\<union>((supp t1)-{x})"
-  apply (nominal_induct t1 avoiding: x t2 rule: trmI.induct)
+  apply (nominal_induct t1 avoiding: x t2 rule: trmI.strong_induct)
   apply (auto simp add: Isubst.simps trmI.supp supp_atm abs_supp supp_nat)
   apply blast+
   done
diff -r 003b5781b845 -r 071f40487734 src/HOL/Nominal/Examples/Contexts.thy
--- a/src/HOL/Nominal/Examples/Contexts.thy	Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/Contexts.thy	Thu May 22 16:34:41 2008 +0200
@@ -93,7 +93,7 @@
   
 lemma ctx_compose:
   shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
-by (induct E1 rule: ctx.weak_induct) (auto)
+by (induct E1 rule: ctx.induct) (auto)
 
 text {* Beta-reduction via contexts in the Felleisen-Hieb style. *}
 
@@ -118,7 +118,7 @@
   assumes a: "t \<longrightarrow>o t'"
   shows "E\<lbrakk>t\<rbrakk> \<longrightarrow>o E\<lbrakk>t'\<rbrakk>"
 using a
-by (induct E rule: ctx.weak_induct) (auto)
+by (induct E rule: ctx.induct) (auto)
 
 lemma ctx_red_in_ctx:
   assumes a: "t \<longrightarrow>x t'"
diff -r 003b5781b845 -r 071f40487734 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Thu May 22 16:34:41 2008 +0200
@@ -34,7 +34,7 @@
   fixes T::"ty"
   and   pi::"name prm"
   shows "pi\<bullet>T = T"
-  by (induct T rule: ty.weak_induct) (simp_all)
+  by (induct T rule: ty.induct) (simp_all)
 
 lemma fresh_ty[simp]:
   fixes x::"name" 
@@ -45,7 +45,7 @@
 lemma ty_cases:
   fixes T::ty
   shows "(\<exists> T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2) \<or> T=TUnit \<or> T=TBase"
-by (induct T rule:ty.weak_induct) (auto)
+by (induct T rule:ty.induct) (auto)
 
 instance ty :: size ..
 
@@ -58,7 +58,7 @@
 lemma ty_size_greater_zero[simp]:
   fixes T::"ty"
   shows "size T > 0"
-by (nominal_induct rule:ty.induct) (simp_all)
+by (nominal_induct rule: ty.strong_induct) (simp_all)
 
 section {* Substitutions *}
 
@@ -119,7 +119,7 @@
 lemma subst_eqvt[eqvt]:
   fixes pi::"name prm" 
   shows "pi\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]"
-  by (nominal_induct t avoiding: x t' rule: trm.induct)
+  by (nominal_induct t avoiding: x t' rule: trm.strong_induct)
      (perm_simp add: fresh_bij)+
 
 lemma subst_rename: 
@@ -127,7 +127,7 @@
   assumes a: "c\<sharp>t\<^isub>1"
   shows "t\<^isub>1[a::=t\<^isub>2] = ([(c,a)]\<bullet>t\<^isub>1)[c::=t\<^isub>2]"
 using a
-apply(nominal_induct t\<^isub>1 avoiding: a c t\<^isub>2 rule: trm.induct)
+apply(nominal_induct t\<^isub>1 avoiding: a c t\<^isub>2 rule: trm.strong_induct)
 apply(simp add: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)+
 done
 
@@ -136,7 +136,7 @@
   assumes a: "z\<sharp>t" "z\<sharp>\<theta>"
   shows "z\<sharp>(\<theta><t>)"
 using a
-by (nominal_induct t avoiding: z \<theta> t rule: trm.induct)
+by (nominal_induct t avoiding: z \<theta> t rule: trm.strong_induct)
    (auto simp add: abs_fresh lookup_fresh)
 
 lemma fresh_subst'':
@@ -144,7 +144,7 @@
   assumes "z\<sharp>t\<^isub>2"
   shows "z\<sharp>t\<^isub>1[z::=t\<^isub>2]"
 using assms 
-by (nominal_induct t\<^isub>1 avoiding: t\<^isub>2 z rule: trm.induct)
+by (nominal_induct t\<^isub>1 avoiding: t\<^isub>2 z rule: trm.strong_induct)
    (auto simp add: abs_fresh fresh_nat fresh_atm)
 
 lemma fresh_subst':
@@ -152,7 +152,7 @@
   assumes "z\<sharp>[y].t\<^isub>1" "z\<sharp>t\<^isub>2"
   shows "z\<sharp>t\<^isub>1[y::=t\<^isub>2]"
 using assms 
-by (nominal_induct t\<^isub>1 avoiding: y t\<^isub>2 z rule: trm.induct)
+by (nominal_induct t\<^isub>1 avoiding: y t\<^isub>2 z rule: trm.strong_induct)
    (auto simp add: abs_fresh fresh_nat fresh_atm)
 
 lemma fresh_subst:
@@ -166,7 +166,7 @@
   assumes "x\<sharp>t"
   shows "((x,u)#\<theta>)<t> = \<theta><t>" 
 using assms
-proof (nominal_induct t avoiding: x u \<theta> rule: trm.induct)
+proof (nominal_induct t avoiding: x u \<theta> rule: trm.strong_induct)
   case (Lam y t x u)
   have fs: "y\<sharp>\<theta>" "y\<sharp>x" "y\<sharp>u" by fact+
   moreover have "x\<sharp> Lam [y].t" by fact 
@@ -184,7 +184,7 @@
   assumes a: "x\<sharp>t" 
   shows "t[x::=t'] = t"
   using a
-by (nominal_induct t avoiding: x t' rule: trm.induct)
+by (nominal_induct t avoiding: x t' rule: trm.strong_induct)
    (auto simp add: fresh_atm abs_fresh)
 
 lemma subst_fun_eq:
@@ -207,14 +207,14 @@
 
 lemma psubst_empty[simp]:
   shows "[]<t> = t"
-by (nominal_induct t rule: trm.induct) 
+by (nominal_induct t rule: trm.strong_induct) 
    (auto simp add: fresh_list_nil)
 
 lemma psubst_subst_psubst:
   assumes h:"c\<sharp>\<theta>"
   shows "\<theta><t>[c::=s] = ((c,s)#\<theta>)<t>"
   using h
-by (nominal_induct t avoiding: \<theta> c s rule: trm.induct)
+by (nominal_induct t avoiding: \<theta> c s rule: trm.strong_induct)
    (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst)
 
 lemma subst_fresh_simp:
@@ -227,7 +227,7 @@
   assumes "x\<sharp>\<theta>" 
   shows "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]"
 using assms
-proof (nominal_induct t avoiding: x u \<theta> rule: trm.induct)
+proof (nominal_induct t avoiding: x u \<theta> rule: trm.strong_induct)
   case (Var n x u \<theta>)
   { assume "x=n"
     moreover have "x\<sharp>\<theta>" by fact 
@@ -654,7 +654,7 @@
 lemma main_lemma:
   shows "\<Gamma> \<turnstile> s is t : T \<Longrightarrow> valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T" 
     and "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> \<Gamma> \<turnstile> p is q : T"
-proof (nominal_induct T arbitrary: \<Gamma> s t p q rule: ty.induct)
+proof (nominal_induct T arbitrary: \<Gamma> s t p q rule: ty.strong_induct)
   case (Arrow T\<^isub>1 T\<^isub>2)
   { 
     case (1 \<Gamma> s t)
@@ -704,14 +704,14 @@
   assumes a: "\<Gamma> \<turnstile> s is t : T"
   shows "\<Gamma> \<turnstile> t is s : T"
 using a 
-by (nominal_induct arbitrary: \<Gamma> s t rule: ty.induct) 
+by (nominal_induct arbitrary: \<Gamma> s t rule: ty.strong_induct) 
    (auto simp add: algorithmic_symmetry)
 
 lemma logical_transitivity:
   assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma> \<turnstile> t is u : T" 
   shows "\<Gamma> \<turnstile> s is u : T"
 using assms
-proof (nominal_induct arbitrary: \<Gamma> s t u  rule:ty.induct)
+proof (nominal_induct arbitrary: \<Gamma> s t u  rule:ty.strong_induct)
   case TBase
   then show "\<Gamma> \<turnstile> s is u : TBase" by (auto elim:  algorithmic_transitivity)
 next 
@@ -738,14 +738,14 @@
   and     c: "t' \<leadsto> t"
   shows "\<Gamma> \<turnstile> s' is t' : T"
 using a b c algorithmic_weak_head_closure 
-by (nominal_induct arbitrary: \<Gamma> s t s' t' rule: ty.induct) 
+by (nominal_induct arbitrary: \<Gamma> s t s' t' rule: ty.strong_induct) 
    (auto, blast)
 
 lemma logical_weak_head_closure':
   assumes "\<Gamma> \<turnstile> s is t : T" and "s' \<leadsto> s" 
   shows "\<Gamma> \<turnstile> s' is t : T"
 using assms
-proof (nominal_induct arbitrary: \<Gamma> s t s' rule: ty.induct)
+proof (nominal_induct arbitrary: \<Gamma> s t s' rule: ty.strong_induct)
   case (TBase  \<Gamma> s t s')
   then show ?case by force
 next
diff -r 003b5781b845 -r 071f40487734 src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Thu May 22 16:34:41 2008 +0200
@@ -156,7 +156,7 @@
   fixes pi::"vrs prm"
   and   S::"ty"
   shows "pi\<bullet>S = S"
-by (induct S rule: ty.weak_induct) (auto simp add: calc_atm)
+by (induct S rule: ty.induct) (auto simp add: calc_atm)
 
 lemma ty_context_vrs_prm_simp:
   fixes pi::"vrs prm"
@@ -341,7 +341,7 @@
   and b: "T closed_in \<Gamma>"
   shows "\<Gamma> \<turnstile> T <: T"
 using a b
-proof(nominal_induct T avoiding: \<Gamma> rule: ty.induct)
+proof(nominal_induct T avoiding: \<Gamma> rule: ty.strong_induct)
   case (Forall X T\<^isub>1 T\<^isub>2)
   have ih_T\<^isub>1: "\<And>\<Gamma>. \<lbrakk>\<turnstile> \<Gamma> ok; T\<^isub>1 closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>1 <: T\<^isub>1" by fact 
   have ih_T\<^isub>2: "\<And>\<Gamma>. \<lbrakk>\<turnstile> \<Gamma> ok; T\<^isub>2 closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>2" by fact
@@ -364,7 +364,7 @@
   and     b: "T closed_in \<Gamma>"
   shows "\<Gamma> \<turnstile> T <: T"
 using a b
-apply(nominal_induct T avoiding: \<Gamma> rule: ty.induct)
+apply(nominal_induct T avoiding: \<Gamma> rule: ty.strong_induct)
 apply(auto simp add: ty.supp abs_supp supp_atm closed_in_def)
   --{* Too bad that this instantiation cannot be found automatically by
   \isakeyword{auto}; \isakeyword{blast} would find it if we had not used 
diff -r 003b5781b845 -r 071f40487734 src/HOL/Nominal/Examples/Height.thy
--- a/src/HOL/Nominal/Examples/Height.thy	Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/Height.thy	Thu May 22 16:34:41 2008 +0200
@@ -49,7 +49,7 @@
 
 lemma height_ge_one: 
   shows "1 \<le> (height e)"
-by (nominal_induct e rule: lam.induct) (simp_all)
+by (nominal_induct e rule: lam.strong_induct) (simp_all)
 
 text {* 
   Unlike the proplem suggested by Wang, however, the 
@@ -58,7 +58,7 @@
 
 theorem height_subst:
   shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')"
-proof (nominal_induct e avoiding: x e' rule: lam.induct)
+proof (nominal_induct e avoiding: x e' rule: lam.strong_induct)
   case (Var y)
   have "1 \<le> height e'" by (rule height_ge_one)
   then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp
diff -r 003b5781b845 -r 071f40487734 src/HOL/Nominal/Examples/Lam_Funs.thy
--- a/src/HOL/Nominal/Examples/Lam_Funs.thy	Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/Lam_Funs.thy	Thu May 22 16:34:41 2008 +0200
@@ -61,7 +61,7 @@
 
 lemma frees_equals_support:
   shows "frees t = supp t"
-by (nominal_induct t rule: lam.induct)
+by (nominal_induct t rule: lam.strong_induct)
    (simp_all add: lam.supp supp_atm abs_supp)
 
 text {* Parallel and single capture-avoiding substitution. *}
@@ -96,7 +96,7 @@
   fixes pi::"name prm" 
   and   t::"lam"
   shows "pi\<bullet>(\<theta><t>) = (pi\<bullet>\<theta>)<(pi\<bullet>t)>"
-by (nominal_induct t avoiding: \<theta> rule: lam.induct)
+by (nominal_induct t avoiding: \<theta> rule: lam.strong_induct)
    (simp_all add: eqvts fresh_bij)
 
 abbreviation 
@@ -112,7 +112,7 @@
 
 lemma subst_supp: 
   shows "supp(t1[a::=t2]) \<subseteq> (((supp(t1)-{a})\<union>supp(t2))::name set)"
-apply(nominal_induct t1 avoiding: a t2 rule: lam.induct)
+apply(nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
 apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp)
 apply(blast)+
 done
@@ -154,6 +154,6 @@
   
 lemma clam_compose:
   shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
-by (induct E1 rule: clam.weak_induct) (auto)
+by (induct E1 rule: clam.induct) (auto)
 
 end
diff -r 003b5781b845 -r 071f40487734 src/HOL/Nominal/Examples/LocalWeakening.thy
--- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Thu May 22 16:34:41 2008 +0200
@@ -26,7 +26,7 @@
 lemma llam_cases:
   "(\<exists>a. t = lPar a) \<or> (\<exists>n. t = lVar n) \<or> (\<exists>t1 t2. t = lApp t1 t2) \<or> 
    (\<exists>t1. t = lLam t1)"
-by (induct t rule: llam.weak_induct)
+by (induct t rule: llam.induct)
    (auto simp add: llam.inject)
 
 consts llam_size :: "llam \<Rightarrow> nat"
@@ -61,7 +61,7 @@
 lemma vsub_eqvt[eqvt]:
   fixes pi::"name prm" 
   shows "pi\<bullet>(vsub t n s) = vsub (pi\<bullet>t) (pi\<bullet>n) (pi\<bullet>s)"
-by (induct t arbitrary: n rule: llam.weak_induct)
+by (induct t arbitrary: n rule: llam.induct)
    (simp_all add: perm_nat_def)
 
 constdefs
@@ -83,7 +83,7 @@
   fixes x::"name"
   and   T::"ty"
   shows "x\<sharp>T"
-by (induct T rule: ty.weak_induct) 
+by (induct T rule: ty.induct) 
    (simp_all add: fresh_nat)
 
 text {* valid contexts *}
diff -r 003b5781b845 -r 071f40487734 src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy	Thu May 22 16:34:41 2008 +0200
@@ -12,14 +12,14 @@
   assumes a: "c\<sharp>t1"
   shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]"
 using a
-by (nominal_induct t1 avoiding: a c t2 rule: lam.induct)
+by (nominal_induct t1 avoiding: a c t2 rule: lam.strong_induct)
    (auto simp add: calc_atm fresh_atm abs_fresh)
 
 lemma forget: 
   assumes a: "a\<sharp>t1"
   shows "t1[a::=t2] = t1"
   using a
-by (nominal_induct t1 avoiding: a t2 rule: lam.induct)
+by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
    (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_fact: 
@@ -27,7 +27,7 @@
   assumes a: "a\<sharp>t1" "a\<sharp>t2"
   shows "a\<sharp>t1[b::=t2]"
 using a
-by (nominal_induct t1 avoiding: a b t2 rule: lam.induct)
+by (nominal_induct t1 avoiding: a b t2 rule: lam.strong_induct)
    (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_fact': 
@@ -35,7 +35,7 @@
   assumes a: "a\<sharp>t2"
   shows "a\<sharp>t1[a::=t2]"
 using a 
-by (nominal_induct t1 avoiding: a t2 rule: lam.induct)
+by (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
    (auto simp add: abs_fresh fresh_atm)
 
 lemma subst_lemma:  
@@ -43,12 +43,12 @@
   and     b: "x\<sharp>L"
   shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"
 using a b
-by (nominal_induct M avoiding: x y N L rule: lam.induct)
+by (nominal_induct M avoiding: x y N L rule: lam.strong_induct)
    (auto simp add: fresh_fact forget)
 
 lemma id_subs: 
   shows "t[x::=Var x] = t"
-  by (nominal_induct t avoiding: x rule: lam.induct)
+  by (nominal_induct t avoiding: x rule: lam.strong_induct)
      (simp_all add: fresh_atm)
 
 lemma lookup_fresh:
@@ -69,7 +69,7 @@
   assumes h:"c\<sharp>\<theta>"
   shows "(\<theta><t>)[c::=s] = ((c,s)#\<theta>)<t>"
   using h
-by (nominal_induct t avoiding: \<theta> c s rule: lam.induct)
+by (nominal_induct t avoiding: \<theta> c s rule: lam.strong_induct)
    (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh')
  
 inductive 
@@ -122,7 +122,7 @@
   fixes a ::"name"
   and   \<tau>  ::"ty"
   shows "a\<sharp>\<tau>"
-by (nominal_induct \<tau> rule: ty.induct)
+by (nominal_induct \<tau> rule: ty.strong_induct)
    (auto simp add: fresh_nat)
 
 (* valid contexts *)
@@ -354,7 +354,7 @@
 text {* properties of the candiadates *}
 lemma RED_props: 
   shows "CR1 \<tau>" and "CR2 \<tau>" and "CR3 \<tau>"
-proof (nominal_induct \<tau> rule: ty.induct)
+proof (nominal_induct \<tau> rule: ty.strong_induct)
   case (TVar a)
   { case 1 show "CR1 (TVar a)" by (simp add: CR1_def)
   next
@@ -553,7 +553,7 @@
 
 lemma id_apply:  
   shows "(id \<Gamma>)<t> = t"
-by (nominal_induct t avoiding: \<Gamma> rule: lam.induct)
+by (nominal_induct t avoiding: \<Gamma> rule: lam.strong_induct)
    (auto simp add: id_maps id_fresh)
 
 lemma id_closes:
diff -r 003b5781b845 -r 071f40487734 src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Thu May 22 16:34:41 2008 +0200
@@ -31,7 +31,7 @@
   fixes x::"name" 
   and   T::"ty"
   shows "x\<sharp>T"
-by (induct T rule: ty.weak_induct)
+by (induct T rule: ty.induct)
    (auto simp add: fresh_nat)
 
 text {* Parallel and single substitution. *}
@@ -80,7 +80,7 @@
   fixes pi::"name prm" 
   and   t::"trm"
   shows "pi\<bullet>(\<theta><t>) = (pi\<bullet>\<theta>)<(pi\<bullet>t)>"
-by (nominal_induct t avoiding: \<theta> rule: trm.induct)
+by (nominal_induct t avoiding: \<theta> rule: trm.strong_induct)
    (perm_simp add: fresh_bij lookup_eqvt)+
 
 lemma fresh_psubst: 
@@ -89,12 +89,12 @@
   assumes "z\<sharp>t" and "z\<sharp>\<theta>"
   shows "z\<sharp>(\<theta><t>)"
 using assms
-by (nominal_induct t avoiding: z \<theta> t rule: trm.induct)
+by (nominal_induct t avoiding: z \<theta> t rule: trm.strong_induct)
    (auto simp add: abs_fresh lookup_fresh)
 
 lemma psubst_empty[simp]:
   shows "[]<t> = t"
-  by (nominal_induct t rule: trm.induct) 
+  by (nominal_induct t rule: trm.strong_induct) 
      (auto simp add: fresh_list_nil)
 
 text {* Single substitution *}
@@ -116,28 +116,28 @@
   assumes a: "z\<sharp>t\<^isub>1" "z\<sharp>t\<^isub>2"
   shows "z\<sharp>t\<^isub>1[y::=t\<^isub>2]"
 using a
-by (nominal_induct t\<^isub>1 avoiding: z y t\<^isub>2 rule: trm.induct)
+by (nominal_induct t\<^isub>1 avoiding: z y t\<^isub>2 rule: trm.strong_induct)
    (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_subst':
   assumes "x\<sharp>e'"
   shows "x\<sharp>e[x::=e']"
   using assms 
-by (nominal_induct e avoiding: x e' rule: trm.induct)
+by (nominal_induct e avoiding: x e' rule: trm.strong_induct)
    (auto simp add: fresh_atm abs_fresh fresh_nat) 
 
 lemma forget: 
   assumes a: "x\<sharp>e" 
   shows "e[x::=e'] = e"
 using a
-by (nominal_induct e avoiding: x e' rule: trm.induct)
+by (nominal_induct e avoiding: x e' rule: trm.strong_induct)
    (auto simp add: fresh_atm abs_fresh)
 
 lemma psubst_subst_psubst:
   assumes h: "x\<sharp>\<theta>"
   shows "\<theta><e>[x::=e'] = ((x,e')#\<theta>)<e>"
   using h
-by (nominal_induct e avoiding: \<theta> x e' rule: trm.induct)
+by (nominal_induct e avoiding: \<theta> x e' rule: trm.strong_induct)
    (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh')
 
 text {* Typing Judgements *}
@@ -264,7 +264,7 @@
   and     "\<Gamma> \<turnstile> e': T'" 
   shows "\<Gamma> \<turnstile> e[x::=e'] : T"
   using assms
-proof (nominal_induct e avoiding: \<Gamma> e' x arbitrary: T rule: trm.induct)
+proof (nominal_induct e avoiding: \<Gamma> e' x arbitrary: T rule: trm.strong_induct)
   case (Var y \<Gamma> e' x T)
   have h1: "(x,T')#\<Gamma> \<turnstile> Var y : T" by fact
   have h2: "\<Gamma> \<turnstile> e' : T'" by fact
@@ -421,7 +421,7 @@
   assumes a: "x\<in>V T"
   shows "(pi\<bullet>x)\<in>V T"
 using a
-apply(nominal_induct T arbitrary: pi x rule: ty.induct)
+apply(nominal_induct T arbitrary: pi x rule: ty.strong_induct)
 apply(auto simp add: trm.inject)
 apply(simp add: eqvts)
 apply(rule_tac x="pi\<bullet>xa" in exI)
@@ -477,7 +477,7 @@
 lemma Vs_are_values:
   assumes a: "e \<in> V T"
   shows "val e"
-using a by (nominal_induct T arbitrary: e rule: ty.induct) (auto)
+using a by (nominal_induct T arbitrary: e rule: ty.strong_induct) (auto)
 
 lemma values_reduce_to_themselves:
   assumes a: "val v"
@@ -531,7 +531,7 @@
   and     h2: "\<theta> Vcloses \<Gamma>"
   shows "\<exists>v. \<theta><e> \<Down> v \<and> v \<in> V T" 
 using h2 h1
-proof(nominal_induct e avoiding: \<Gamma> \<theta> arbitrary: T rule: trm.induct)
+proof(nominal_induct e avoiding: \<Gamma> \<theta> arbitrary: T rule: trm.strong_induct)
   case (App e\<^isub>1 e\<^isub>2 \<Gamma> \<theta> T)
   have ih\<^isub>1:"\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e\<^isub>1 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e\<^isub>1> \<Down> v \<and> v \<in> V T" by fact
   have ih\<^isub>2:"\<And>\<theta> \<Gamma> T. \<lbrakk>\<theta> Vcloses \<Gamma>; \<Gamma> \<turnstile> e\<^isub>2 : T\<rbrakk> \<Longrightarrow> \<exists>v. \<theta><e\<^isub>2> \<Down> v \<and> v \<in> V T" by fact
diff -r 003b5781b845 -r 071f40487734 src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Thu May 22 16:34:41 2008 +0200
@@ -26,7 +26,7 @@
   fixes x::"name"
   and   T::"ty"
   shows "x\<sharp>T"
-by (nominal_induct T rule: ty.induct)
+by (nominal_induct T rule: ty.strong_induct)
    (auto simp add: fresh_string)
 
 text {* 
diff -r 003b5781b845 -r 071f40487734 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Wed May 21 22:04:58 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Thu May 22 16:34:41 2008 +0200
@@ -1094,8 +1094,8 @@
  
     val (_, thy9) = thy8 |>
       Sign.add_path big_name |>
-      PureThy.add_thms [(("weak_induct", dt_induct), [case_names_induct])] ||>>
-      PureThy.add_thmss [(("weak_inducts", projections dt_induct), [case_names_induct])] ||>
+      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] ||>>
+      PureThy.add_thmss [(("inducts", projections dt_induct), [case_names_induct])] ||>
       Sign.parent_path ||>>
       DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
       DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
@@ -1378,9 +1378,9 @@
 
     val (_, thy10) = thy9 |>
       Sign.add_path big_name |>
-      PureThy.add_thms [(("induct'", induct_aux), [])] ||>>
-      PureThy.add_thms [(("induct", induct), [case_names_induct])] ||>>
-      PureThy.add_thmss [(("inducts", projections induct), [case_names_induct])];
+      PureThy.add_thms [(("strong_induct'", induct_aux), [])] ||>>
+      PureThy.add_thms [(("strong_induct", induct), [case_names_induct])] ||>>
+      PureThy.add_thmss [(("strong_inducts", projections induct), [case_names_induct])];
 
     (**** recursion combinator ****)