diff -r bb18eed53ed6 -r a1119cf551e8 src/HOL/Nominal/Examples/CR.thy
--- a/src/HOL/Nominal/Examples/CR.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Nominal/Examples/CR.thy	Tue Aug 13 16:25:47 2013 +0200
@@ -146,12 +146,12 @@
 section {* Beta Reduction *}
 
 inductive
-  "Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
+  "Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^sub>\<beta> _" [80,80] 80)
 where
-    b1[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"
-  | b2[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"
-  | b3[intro]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [a].s2)"
-  | b4[intro]: "a\<sharp>s2 \<Longrightarrow> (App (Lam [a].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"
+    b1[intro]: "s1\<longrightarrow>\<^sub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^sub>\<beta>(App s2 t)"
+  | b2[intro]: "s1\<longrightarrow>\<^sub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^sub>\<beta>(App t s2)"
+  | b3[intro]: "s1\<longrightarrow>\<^sub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^sub>\<beta> (Lam [a].s2)"
+  | b4[intro]: "a\<sharp>s2 \<Longrightarrow> (App (Lam [a].s1) s2)\<longrightarrow>\<^sub>\<beta>(s1[a::=s2])"
 
 equivariance Beta
 
@@ -159,29 +159,29 @@
   by (simp_all add: abs_fresh fresh_fact')
 
 inductive
-  "Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
+  "Beta_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^sub>\<beta>\<^sup>* _" [80,80] 80)
 where
-    bs1[intro, simp]: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
-  | bs2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2; M2 \<longrightarrow>\<^isub>\<beta> M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
+    bs1[intro, simp]: "M \<longrightarrow>\<^sub>\<beta>\<^sup>* M"
+  | bs2[intro]: "\<lbrakk>M1\<longrightarrow>\<^sub>\<beta>\<^sup>* M2; M2 \<longrightarrow>\<^sub>\<beta> M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^sub>\<beta>\<^sup>* M3"
 
 equivariance Beta_star
 
 lemma beta_star_trans:
-  assumes a1: "M1\<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
-  and     a2: "M2\<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
-  shows "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
+  assumes a1: "M1\<longrightarrow>\<^sub>\<beta>\<^sup>* M2"
+  and     a2: "M2\<longrightarrow>\<^sub>\<beta>\<^sup>* M3"
+  shows "M1 \<longrightarrow>\<^sub>\<beta>\<^sup>* M3"
 using a2 a1
 by (induct) (auto)
 
 section {* One-Reduction *}
 
 inductive
-  One :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1 _" [80,80] 80)
+  One :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^sub>1 _" [80,80] 80)
 where
-    o1[intro!]:      "M\<longrightarrow>\<^isub>1M"
-  | o2[simp,intro!]: "\<lbrakk>t1\<longrightarrow>\<^isub>1t2;s1\<longrightarrow>\<^isub>1s2\<rbrakk> \<Longrightarrow> (App t1 s1)\<longrightarrow>\<^isub>1(App t2 s2)"
-  | o3[simp,intro!]: "s1\<longrightarrow>\<^isub>1s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>1(Lam [a].s2)"
-  | o4[simp,intro!]: "\<lbrakk>a\<sharp>(s1,s2); s1\<longrightarrow>\<^isub>1s2;t1\<longrightarrow>\<^isub>1t2\<rbrakk> \<Longrightarrow> (App (Lam [a].t1) s1)\<longrightarrow>\<^isub>1(t2[a::=s2])"
+    o1[intro!]:      "M\<longrightarrow>\<^sub>1M"
+  | o2[simp,intro!]: "\<lbrakk>t1\<longrightarrow>\<^sub>1t2;s1\<longrightarrow>\<^sub>1s2\<rbrakk> \<Longrightarrow> (App t1 s1)\<longrightarrow>\<^sub>1(App t2 s2)"
+  | o3[simp,intro!]: "s1\<longrightarrow>\<^sub>1s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^sub>1(Lam [a].s2)"
+  | o4[simp,intro!]: "\<lbrakk>a\<sharp>(s1,s2); s1\<longrightarrow>\<^sub>1s2;t1\<longrightarrow>\<^sub>1t2\<rbrakk> \<Longrightarrow> (App (Lam [a].t1) s1)\<longrightarrow>\<^sub>1(t2[a::=s2])"
 
 equivariance One
 
@@ -189,23 +189,23 @@
   by (simp_all add: abs_fresh fresh_fact')
 
 inductive
-  "One_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>1\<^sup>* _" [80,80] 80)
+  "One_star"  :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^sub>1\<^sup>* _" [80,80] 80)
 where
-    os1[intro, simp]: "M \<longrightarrow>\<^isub>1\<^sup>* M"
-  | os2[intro]: "\<lbrakk>M1\<longrightarrow>\<^isub>1\<^sup>* M2; M2 \<longrightarrow>\<^isub>1 M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^isub>1\<^sup>* M3"
+    os1[intro, simp]: "M \<longrightarrow>\<^sub>1\<^sup>* M"
+  | os2[intro]: "\<lbrakk>M1\<longrightarrow>\<^sub>1\<^sup>* M2; M2 \<longrightarrow>\<^sub>1 M3\<rbrakk> \<Longrightarrow> M1 \<longrightarrow>\<^sub>1\<^sup>* M3"
 
 equivariance One_star 
 
 lemma one_star_trans:
-  assumes a1: "M1\<longrightarrow>\<^isub>1\<^sup>* M2" 
-  and     a2: "M2\<longrightarrow>\<^isub>1\<^sup>* M3"
-  shows "M1\<longrightarrow>\<^isub>1\<^sup>* M3"
+  assumes a1: "M1\<longrightarrow>\<^sub>1\<^sup>* M2" 
+  and     a2: "M2\<longrightarrow>\<^sub>1\<^sup>* M3"
+  shows "M1\<longrightarrow>\<^sub>1\<^sup>* M3"
 using a2 a1
 by (induct) (auto)
 
 lemma one_fresh_preserv:
   fixes a :: "name"
-  assumes a: "t\<longrightarrow>\<^isub>1s"
+  assumes a: "t\<longrightarrow>\<^sub>1s"
   and     b: "a\<sharp>t"
   shows "a\<sharp>s"
 using a b
@@ -247,7 +247,7 @@
 
 lemma one_fresh_preserv_automatic:
   fixes a :: "name"
-  assumes a: "t\<longrightarrow>\<^isub>1s"
+  assumes a: "t\<longrightarrow>\<^sub>1s"
   and     b: "a\<sharp>t"
   shows "a\<sharp>s"
 using a b
@@ -263,8 +263,8 @@
    (auto simp add: calc_atm fresh_atm abs_fresh)
 
 lemma one_abs: 
-  assumes a: "Lam [a].t\<longrightarrow>\<^isub>1t'"
-  shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>1t''"
+  assumes a: "Lam [a].t\<longrightarrow>\<^sub>1t'"
+  shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^sub>1t''"
 proof -
   have "a\<sharp>Lam [a].t" by (simp add: abs_fresh)
   with a have "a\<sharp>t'" by (simp add: one_fresh_preserv)
@@ -274,15 +274,15 @@
 qed
 
 lemma one_app: 
-  assumes a: "App t1 t2 \<longrightarrow>\<^isub>1 t'"
-  shows "(\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
-         (\<exists>a s s1 s2. t1 = Lam [a].s \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2 \<and> a\<sharp>(t2,s2))"
+  assumes a: "App t1 t2 \<longrightarrow>\<^sub>1 t'"
+  shows "(\<exists>s1 s2. t' = App s1 s2 \<and> t1 \<longrightarrow>\<^sub>1 s1 \<and> t2 \<longrightarrow>\<^sub>1 s2) \<or> 
+         (\<exists>a s s1 s2. t1 = Lam [a].s \<and> t' = s1[a::=s2] \<and> s \<longrightarrow>\<^sub>1 s1 \<and> t2 \<longrightarrow>\<^sub>1 s2 \<and> a\<sharp>(t2,s2))"
 using a by (erule_tac One.cases) (auto simp add: lam.inject)
 
 lemma one_red: 
-  assumes a: "App (Lam [a].t1) t2 \<longrightarrow>\<^isub>1 M" "a\<sharp>(t2,M)"
-  shows "(\<exists>s1 s2. M = App (Lam [a].s1) s2 \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2) \<or> 
-         (\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^isub>1 s1 \<and> t2 \<longrightarrow>\<^isub>1 s2)" 
+  assumes a: "App (Lam [a].t1) t2 \<longrightarrow>\<^sub>1 M" "a\<sharp>(t2,M)"
+  shows "(\<exists>s1 s2. M = App (Lam [a].s1) s2 \<and> t1 \<longrightarrow>\<^sub>1 s1 \<and> t2 \<longrightarrow>\<^sub>1 s2) \<or> 
+         (\<exists>s1 s2. M = s1[a::=s2] \<and> t1 \<longrightarrow>\<^sub>1 s1 \<and> t2 \<longrightarrow>\<^sub>1 s2)" 
 using a
 by (cases rule: One.strong_cases [where a="a" and aa="a"])
    (auto dest: one_abs simp add: lam.inject abs_fresh alpha fresh_prod)
@@ -290,31 +290,31 @@
 text {* first case in Lemma 3.2.4*}
 
 lemma one_subst_aux:
-  assumes a: "N\<longrightarrow>\<^isub>1N'"
-  shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
+  assumes a: "N\<longrightarrow>\<^sub>1N'"
+  shows "M[x::=N] \<longrightarrow>\<^sub>1 M[x::=N']"
 using a
 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
+  thus "Var y[x::=N] \<longrightarrow>\<^sub>1 Var y[x::=N']" by (cases "x=y") auto
 next
   case (App P Q) (* application case - third line *)
-  thus "(App P Q)[x::=N] \<longrightarrow>\<^isub>1  (App P Q)[x::=N']" using o2 by simp
+  thus "(App P Q)[x::=N] \<longrightarrow>\<^sub>1  (App P Q)[x::=N']" using o2 by simp
 next 
   case (Lam y P) (* abstraction case - fourth line *)
-  thus "(Lam [y].P)[x::=N] \<longrightarrow>\<^isub>1 (Lam [y].P)[x::=N']" using o3 by simp
+  thus "(Lam [y].P)[x::=N] \<longrightarrow>\<^sub>1 (Lam [y].P)[x::=N']" using o3 by simp
 qed
 
 lemma one_subst_aux_automatic:
-  assumes a: "N\<longrightarrow>\<^isub>1N'"
-  shows "M[x::=N] \<longrightarrow>\<^isub>1 M[x::=N']"
+  assumes a: "N\<longrightarrow>\<^sub>1N'"
+  shows "M[x::=N] \<longrightarrow>\<^sub>1 M[x::=N']"
 using a
 by (nominal_induct M avoiding: x N N' rule: lam.strong_induct)
    (auto simp add: fresh_prod fresh_atm)
 
 lemma one_subst: 
-  assumes a: "M\<longrightarrow>\<^isub>1M'"
-  and     b: "N\<longrightarrow>\<^isub>1N'"
-  shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
+  assumes a: "M\<longrightarrow>\<^sub>1M'"
+  and     b: "N\<longrightarrow>\<^sub>1N'"
+  shows "M[x::=N]\<longrightarrow>\<^sub>1M'[x::=N']" 
 using a b
 proof (nominal_induct M M' avoiding: N N' x rule: One.strong_induct)
   case (o1 M)
@@ -328,22 +328,22 @@
 next
   case (o4 a N1 N2 M1 M2 N N' x)
   have vc: "a\<sharp>N" "a\<sharp>N'" "a\<sharp>x" "a\<sharp>N1" "a\<sharp>N2" by fact+
-  have asm: "N\<longrightarrow>\<^isub>1N'" by fact
+  have asm: "N\<longrightarrow>\<^sub>1N'" by fact
   show ?case
   proof -
     have "(App (Lam [a].M1) N1)[x::=N] = App (Lam [a].(M1[x::=N])) (N1[x::=N])" using vc by simp
-    moreover have "App (Lam [a].(M1[x::=N])) (N1[x::=N]) \<longrightarrow>\<^isub>1 M2[x::=N'][a::=N2[x::=N']]" 
+    moreover have "App (Lam [a].(M1[x::=N])) (N1[x::=N]) \<longrightarrow>\<^sub>1 M2[x::=N'][a::=N2[x::=N']]" 
       using o4 asm by (simp add: fresh_fact)
     moreover have "M2[x::=N'][a::=N2[x::=N']] = M2[a::=N2][x::=N']" 
       using vc by (simp add: substitution_lemma fresh_atm)
-    ultimately show "(App (Lam [a].M1) N1)[x::=N] \<longrightarrow>\<^isub>1 M2[a::=N2][x::=N']" by simp
+    ultimately show "(App (Lam [a].M1) N1)[x::=N] \<longrightarrow>\<^sub>1 M2[a::=N2][x::=N']" by simp
   qed
 qed
 
 lemma one_subst_automatic: 
-  assumes a: "M\<longrightarrow>\<^isub>1M'" 
-  and     b: "N\<longrightarrow>\<^isub>1N'"
-  shows "M[x::=N]\<longrightarrow>\<^isub>1M'[x::=N']" 
+  assumes a: "M\<longrightarrow>\<^sub>1M'" 
+  and     b: "N\<longrightarrow>\<^sub>1N'"
+  shows "M[x::=N]\<longrightarrow>\<^sub>1M'[x::=N']" 
 using a b
 by (nominal_induct M M' avoiding: N N' x rule: One.strong_induct)
    (auto simp add: one_subst_aux substitution_lemma fresh_atm fresh_fact)
@@ -351,122 +351,122 @@
 lemma diamond[rule_format]:
   fixes    M :: "lam"
   and      M1:: "lam"
-  assumes a: "M\<longrightarrow>\<^isub>1M1" 
-  and     b: "M\<longrightarrow>\<^isub>1M2"
-  shows "\<exists>M3. M1\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3"
+  assumes a: "M\<longrightarrow>\<^sub>1M1" 
+  and     b: "M\<longrightarrow>\<^sub>1M2"
+  shows "\<exists>M3. M1\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3"
   using a b
 proof (nominal_induct avoiding: M1 M2 rule: One.strong_induct)
   case (o1 M) (* case 1 --- M1 = M *)
-  thus "\<exists>M3. M\<longrightarrow>\<^isub>1M3 \<and>  M2\<longrightarrow>\<^isub>1M3" by blast
+  thus "\<exists>M3. M\<longrightarrow>\<^sub>1M3 \<and>  M2\<longrightarrow>\<^sub>1M3" by blast
 next
   case (o4 x Q Q' P P') (* case 2 --- a beta-reduction occurs*)
   have vc: "x\<sharp>Q" "x\<sharp>Q'" "x\<sharp>M2" by fact+
-  have i1: "\<And>M2. Q \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
-  have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
-  have "App (Lam [x].P) Q \<longrightarrow>\<^isub>1 M2" by fact
-  hence "(\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q') \<or> 
-         (\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q')" using vc by (simp add: one_red)
+  have i1: "\<And>M2. Q \<longrightarrow>\<^sub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3)" by fact
+  have i2: "\<And>M2. P \<longrightarrow>\<^sub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3)" by fact
+  have "App (Lam [x].P) Q \<longrightarrow>\<^sub>1 M2" by fact
+  hence "(\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^sub>1P' \<and> Q\<longrightarrow>\<^sub>1Q') \<or> 
+         (\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^sub>1P' \<and> Q\<longrightarrow>\<^sub>1Q')" using vc by (simp add: one_red)
   moreover (* subcase 2.1 *)
-  { assume "\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q'"
+  { assume "\<exists>P' Q'. M2 = App (Lam [x].P') Q' \<and> P\<longrightarrow>\<^sub>1P' \<and> Q\<longrightarrow>\<^sub>1Q'"
     then obtain P'' and Q'' where 
-      b1: "M2=App (Lam [x].P'') Q''" and b2: "P\<longrightarrow>\<^isub>1P''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by blast
-    from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp
+      b1: "M2=App (Lam [x].P'') Q''" and b2: "P\<longrightarrow>\<^sub>1P''" and b3: "Q\<longrightarrow>\<^sub>1Q''" by blast
+    from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^sub>1M3 \<and> P''\<longrightarrow>\<^sub>1M3)" by simp
     then obtain P''' where
-      c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by force
-    from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp
+      c1: "P'\<longrightarrow>\<^sub>1P'''" and c2: "P''\<longrightarrow>\<^sub>1P'''" by force
+    from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^sub>1M3 \<and> Q''\<longrightarrow>\<^sub>1M3)" by simp
     then obtain Q''' where
-      d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by force
+      d1: "Q'\<longrightarrow>\<^sub>1Q'''" and d2: "Q''\<longrightarrow>\<^sub>1Q'''" by force
     from c1 c2 d1 d2 
-    have "P'[x::=Q']\<longrightarrow>\<^isub>1P'''[x::=Q'''] \<and> App (Lam [x].P'') Q'' \<longrightarrow>\<^isub>1 P'''[x::=Q''']" 
+    have "P'[x::=Q']\<longrightarrow>\<^sub>1P'''[x::=Q'''] \<and> App (Lam [x].P'') Q'' \<longrightarrow>\<^sub>1 P'''[x::=Q''']" 
       using vc b3 by (auto simp add: one_subst one_fresh_preserv)
-    hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast
+    hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" using b1 by blast
   }
   moreover (* subcase 2.2 *)
-  { assume "\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^isub>1P' \<and> Q\<longrightarrow>\<^isub>1Q'"
+  { assume "\<exists>P' Q'. M2 = P'[x::=Q'] \<and> P\<longrightarrow>\<^sub>1P' \<and> Q\<longrightarrow>\<^sub>1Q'"
     then obtain P'' Q'' where
-      b1: "M2=P''[x::=Q'']" and b2: "P\<longrightarrow>\<^isub>1P''" and  b3: "Q\<longrightarrow>\<^isub>1Q''" by blast
-    from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp
+      b1: "M2=P''[x::=Q'']" and b2: "P\<longrightarrow>\<^sub>1P''" and  b3: "Q\<longrightarrow>\<^sub>1Q''" by blast
+    from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^sub>1M3 \<and> P''\<longrightarrow>\<^sub>1M3)" by simp
     then obtain P''' where
-      c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by blast
-    from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp
+      c1: "P'\<longrightarrow>\<^sub>1P'''" and c2: "P''\<longrightarrow>\<^sub>1P'''" by blast
+    from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^sub>1M3 \<and> Q''\<longrightarrow>\<^sub>1M3)" by simp
     then obtain Q''' where
-      d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by blast
+      d1: "Q'\<longrightarrow>\<^sub>1Q'''" and d2: "Q''\<longrightarrow>\<^sub>1Q'''" by blast
     from c1 c2 d1 d2 
-    have "P'[x::=Q']\<longrightarrow>\<^isub>1P'''[x::=Q'''] \<and> P''[x::=Q'']\<longrightarrow>\<^isub>1P'''[x::=Q''']" 
+    have "P'[x::=Q']\<longrightarrow>\<^sub>1P'''[x::=Q'''] \<and> P''[x::=Q'']\<longrightarrow>\<^sub>1P'''[x::=Q''']" 
       by (force simp add: one_subst)
-    hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast
+    hence "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" using b1 by blast
   }
-  ultimately show "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast
+  ultimately show "\<exists>M3. P'[x::=Q']\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" by blast
 next
   case (o2 P P' Q Q') (* case 3 *)
-  have i0: "P\<longrightarrow>\<^isub>1P'" by fact
-  have i0': "Q\<longrightarrow>\<^isub>1Q'" by fact
-  have i1: "\<And>M2. Q \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
-  have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
-  assume "App P Q \<longrightarrow>\<^isub>1 M2"
-  hence "(\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q'') \<or> 
-         (\<exists>x P' P'' Q'. P = Lam [x].P' \<and> M2 = P''[x::=Q'] \<and> P'\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q' \<and> x\<sharp>(Q,Q'))" 
+  have i0: "P\<longrightarrow>\<^sub>1P'" by fact
+  have i0': "Q\<longrightarrow>\<^sub>1Q'" by fact
+  have i1: "\<And>M2. Q \<longrightarrow>\<^sub>1M2 \<Longrightarrow> (\<exists>M3. Q'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3)" by fact
+  have i2: "\<And>M2. P \<longrightarrow>\<^sub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3)" by fact
+  assume "App P Q \<longrightarrow>\<^sub>1 M2"
+  hence "(\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^sub>1P'' \<and> Q\<longrightarrow>\<^sub>1Q'') \<or> 
+         (\<exists>x P' P'' Q'. P = Lam [x].P' \<and> M2 = P''[x::=Q'] \<and> P'\<longrightarrow>\<^sub>1 P'' \<and> Q\<longrightarrow>\<^sub>1Q' \<and> x\<sharp>(Q,Q'))" 
     by (simp add: one_app[simplified])
   moreover (* subcase 3.1 *)
-  { assume "\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^isub>1P'' \<and> Q\<longrightarrow>\<^isub>1Q''"
+  { assume "\<exists>P'' Q''. M2 = App P'' Q'' \<and> P\<longrightarrow>\<^sub>1P'' \<and> Q\<longrightarrow>\<^sub>1Q''"
     then obtain P'' and Q'' where 
-      b1: "M2=App P'' Q''" and b2: "P\<longrightarrow>\<^isub>1P''" and b3: "Q\<longrightarrow>\<^isub>1Q''" by blast
-    from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> P''\<longrightarrow>\<^isub>1M3)" by simp
+      b1: "M2=App P'' Q''" and b2: "P\<longrightarrow>\<^sub>1P''" and b3: "Q\<longrightarrow>\<^sub>1Q''" by blast
+    from b2 i2 have "(\<exists>M3. P'\<longrightarrow>\<^sub>1M3 \<and> P''\<longrightarrow>\<^sub>1M3)" by simp
     then obtain P''' where
-      c1: "P'\<longrightarrow>\<^isub>1P'''" and c2: "P''\<longrightarrow>\<^isub>1P'''" by blast
-    from b3 i1 have "\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3" by simp
+      c1: "P'\<longrightarrow>\<^sub>1P'''" and c2: "P''\<longrightarrow>\<^sub>1P'''" by blast
+    from b3 i1 have "\<exists>M3. Q'\<longrightarrow>\<^sub>1M3 \<and> Q''\<longrightarrow>\<^sub>1M3" by simp
     then obtain Q''' where
-      d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by blast
+      d1: "Q'\<longrightarrow>\<^sub>1Q'''" and d2: "Q''\<longrightarrow>\<^sub>1Q'''" by blast
     from c1 c2 d1 d2 
-    have "App P' Q'\<longrightarrow>\<^isub>1App P''' Q''' \<and> App P'' Q'' \<longrightarrow>\<^isub>1 App P''' Q'''" by blast
-    hence "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast
+    have "App P' Q'\<longrightarrow>\<^sub>1App P''' Q''' \<and> App P'' Q'' \<longrightarrow>\<^sub>1 App P''' Q'''" by blast
+    hence "\<exists>M3. App P' Q'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" using b1 by blast
   }
   moreover (* subcase 3.2 *)
-  { assume "\<exists>x P1 P'' Q''. P = Lam [x].P1 \<and> M2 = P''[x::=Q''] \<and> P1\<longrightarrow>\<^isub>1 P'' \<and> Q\<longrightarrow>\<^isub>1Q'' \<and> x\<sharp>(Q,Q'')"
+  { assume "\<exists>x P1 P'' Q''. P = Lam [x].P1 \<and> M2 = P''[x::=Q''] \<and> P1\<longrightarrow>\<^sub>1 P'' \<and> Q\<longrightarrow>\<^sub>1Q'' \<and> x\<sharp>(Q,Q'')"
     then obtain x P1 P1'' Q'' where
       b0: "P = Lam [x].P1" and b1: "M2 = P1''[x::=Q'']" and 
-      b2: "P1\<longrightarrow>\<^isub>1P1''" and  b3: "Q\<longrightarrow>\<^isub>1Q''" and vc: "x\<sharp>(Q,Q'')" by blast
-    from b0 i0 have "\<exists>P1'. P'=Lam [x].P1' \<and> P1\<longrightarrow>\<^isub>1P1'" by (simp add: one_abs)      
-    then obtain P1' where g1: "P'=Lam [x].P1'" and g2: "P1\<longrightarrow>\<^isub>1P1'" by blast 
-    from g1 b0 b2 i2 have "(\<exists>M3. (Lam [x].P1')\<longrightarrow>\<^isub>1M3 \<and> (Lam [x].P1'')\<longrightarrow>\<^isub>1M3)" by simp
+      b2: "P1\<longrightarrow>\<^sub>1P1''" and  b3: "Q\<longrightarrow>\<^sub>1Q''" and vc: "x\<sharp>(Q,Q'')" by blast
+    from b0 i0 have "\<exists>P1'. P'=Lam [x].P1' \<and> P1\<longrightarrow>\<^sub>1P1'" by (simp add: one_abs)      
+    then obtain P1' where g1: "P'=Lam [x].P1'" and g2: "P1\<longrightarrow>\<^sub>1P1'" by blast 
+    from g1 b0 b2 i2 have "(\<exists>M3. (Lam [x].P1')\<longrightarrow>\<^sub>1M3 \<and> (Lam [x].P1'')\<longrightarrow>\<^sub>1M3)" by simp
     then obtain P1''' where
-      c1: "(Lam [x].P1')\<longrightarrow>\<^isub>1P1'''" and c2: "(Lam [x].P1'')\<longrightarrow>\<^isub>1P1'''" by blast
-    from c1 have "\<exists>R1. P1'''=Lam [x].R1 \<and> P1'\<longrightarrow>\<^isub>1R1" by (simp add: one_abs)
-    then obtain R1 where r1: "P1'''=Lam [x].R1" and r2: "P1'\<longrightarrow>\<^isub>1R1" by blast
-    from c2 have "\<exists>R2. P1'''=Lam [x].R2 \<and> P1''\<longrightarrow>\<^isub>1R2" by (simp add: one_abs)
-    then obtain R2 where r3: "P1'''=Lam [x].R2" and r4: "P1''\<longrightarrow>\<^isub>1R2" by blast
+      c1: "(Lam [x].P1')\<longrightarrow>\<^sub>1P1'''" and c2: "(Lam [x].P1'')\<longrightarrow>\<^sub>1P1'''" by blast
+    from c1 have "\<exists>R1. P1'''=Lam [x].R1 \<and> P1'\<longrightarrow>\<^sub>1R1" by (simp add: one_abs)
+    then obtain R1 where r1: "P1'''=Lam [x].R1" and r2: "P1'\<longrightarrow>\<^sub>1R1" by blast
+    from c2 have "\<exists>R2. P1'''=Lam [x].R2 \<and> P1''\<longrightarrow>\<^sub>1R2" by (simp add: one_abs)
+    then obtain R2 where r3: "P1'''=Lam [x].R2" and r4: "P1''\<longrightarrow>\<^sub>1R2" by blast
     from r1 r3 have r5: "R1=R2" by (simp add: lam.inject alpha)
-    from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^isub>1M3 \<and> Q''\<longrightarrow>\<^isub>1M3)" by simp
+    from b3 i1 have "(\<exists>M3. Q'\<longrightarrow>\<^sub>1M3 \<and> Q''\<longrightarrow>\<^sub>1M3)" by simp
     then obtain Q''' where
-      d1: "Q'\<longrightarrow>\<^isub>1Q'''" and d2: "Q''\<longrightarrow>\<^isub>1Q'''" by blast
+      d1: "Q'\<longrightarrow>\<^sub>1Q'''" and d2: "Q''\<longrightarrow>\<^sub>1Q'''" by blast
     from g1 r2 d1 r4 r5 d2 
-    have "App P' Q'\<longrightarrow>\<^isub>1R1[x::=Q'''] \<and> P1''[x::=Q'']\<longrightarrow>\<^isub>1R1[x::=Q''']" 
+    have "App P' Q'\<longrightarrow>\<^sub>1R1[x::=Q'''] \<and> P1''[x::=Q'']\<longrightarrow>\<^sub>1R1[x::=Q''']" 
       using vc i0' by (simp add: one_subst one_fresh_preserv)
-    hence "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 by blast
+    hence "\<exists>M3. App P' Q'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" using b1 by blast
   }
-  ultimately show "\<exists>M3. App P' Q'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" by blast
+  ultimately show "\<exists>M3. App P' Q'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" by blast
 next
   case (o3 P P' x) (* case 4 *)
-  have i1: "P\<longrightarrow>\<^isub>1P'" by fact
-  have i2: "\<And>M2. P \<longrightarrow>\<^isub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3)" by fact
-  have "(Lam [x].P)\<longrightarrow>\<^isub>1 M2" by fact
-  hence "\<exists>P''. M2=Lam [x].P'' \<and> P\<longrightarrow>\<^isub>1P''" by (simp add: one_abs)
-  then obtain P'' where b1: "M2=Lam [x].P''" and b2: "P\<longrightarrow>\<^isub>1P''" by blast
-  from i2 b1 b2 have "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^isub>1M3 \<and> (Lam [x].P'')\<longrightarrow>\<^isub>1M3" by blast
-  then obtain M3 where c1: "(Lam [x].P')\<longrightarrow>\<^isub>1M3" and c2: "(Lam [x].P'')\<longrightarrow>\<^isub>1M3" by blast
-  from c1 have "\<exists>R1. M3=Lam [x].R1 \<and> P'\<longrightarrow>\<^isub>1R1" by (simp add: one_abs)
-  then obtain R1 where r1: "M3=Lam [x].R1" and r2: "P'\<longrightarrow>\<^isub>1R1" by blast
-  from c2 have "\<exists>R2. M3=Lam [x].R2 \<and> P''\<longrightarrow>\<^isub>1R2" by (simp add: one_abs)
-  then obtain R2 where r3: "M3=Lam [x].R2" and r4: "P''\<longrightarrow>\<^isub>1R2" by blast
+  have i1: "P\<longrightarrow>\<^sub>1P'" by fact
+  have i2: "\<And>M2. P \<longrightarrow>\<^sub>1M2 \<Longrightarrow> (\<exists>M3. P'\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3)" by fact
+  have "(Lam [x].P)\<longrightarrow>\<^sub>1 M2" by fact
+  hence "\<exists>P''. M2=Lam [x].P'' \<and> P\<longrightarrow>\<^sub>1P''" by (simp add: one_abs)
+  then obtain P'' where b1: "M2=Lam [x].P''" and b2: "P\<longrightarrow>\<^sub>1P''" by blast
+  from i2 b1 b2 have "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^sub>1M3 \<and> (Lam [x].P'')\<longrightarrow>\<^sub>1M3" by blast
+  then obtain M3 where c1: "(Lam [x].P')\<longrightarrow>\<^sub>1M3" and c2: "(Lam [x].P'')\<longrightarrow>\<^sub>1M3" by blast
+  from c1 have "\<exists>R1. M3=Lam [x].R1 \<and> P'\<longrightarrow>\<^sub>1R1" by (simp add: one_abs)
+  then obtain R1 where r1: "M3=Lam [x].R1" and r2: "P'\<longrightarrow>\<^sub>1R1" by blast
+  from c2 have "\<exists>R2. M3=Lam [x].R2 \<and> P''\<longrightarrow>\<^sub>1R2" by (simp add: one_abs)
+  then obtain R2 where r3: "M3=Lam [x].R2" and r4: "P''\<longrightarrow>\<^sub>1R2" by blast
   from r1 r3 have r5: "R1=R2" by (simp add: lam.inject alpha)
-  from r2 r4 have "(Lam [x].P')\<longrightarrow>\<^isub>1(Lam [x].R1) \<and> (Lam [x].P'')\<longrightarrow>\<^isub>1(Lam [x].R2)" 
+  from r2 r4 have "(Lam [x].P')\<longrightarrow>\<^sub>1(Lam [x].R1) \<and> (Lam [x].P'')\<longrightarrow>\<^sub>1(Lam [x].R2)" 
     by (simp add: one_subst)
-  thus "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^isub>1M3 \<and> M2\<longrightarrow>\<^isub>1M3" using b1 r5 by blast
+  thus "\<exists>M3. (Lam [x].P')\<longrightarrow>\<^sub>1M3 \<and> M2\<longrightarrow>\<^sub>1M3" using b1 r5 by blast
 qed
 
 lemma one_lam_cong: 
-  assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
-  shows "(Lam [a].t1)\<longrightarrow>\<^isub>\<beta>\<^sup>*(Lam [a].t2)"
+  assumes a: "t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t2" 
+  shows "(Lam [a].t1)\<longrightarrow>\<^sub>\<beta>\<^sup>*(Lam [a].t2)"
   using a
 proof induct
   case bs1 thus ?case by simp
@@ -476,8 +476,8 @@
 qed
 
 lemma one_app_congL: 
-  assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
-  shows "App t1 s\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s"
+  assumes a: "t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t2" 
+  shows "App t1 s\<longrightarrow>\<^sub>\<beta>\<^sup>* App t2 s"
   using a
 proof induct
   case bs1 thus ?case by simp
@@ -486,8 +486,8 @@
 qed
   
 lemma one_app_congR: 
-  assumes a: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
-  shows "App s t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App s t2"
+  assumes a: "t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t2" 
+  shows "App s t1 \<longrightarrow>\<^sub>\<beta>\<^sup>* App s t2"
 using a
 proof induct
   case bs1 thus ?case by simp
@@ -496,19 +496,19 @@
 qed
 
 lemma one_app_cong: 
-  assumes a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
-  and     a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" 
-  shows "App t1 s1\<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2"
+  assumes a1: "t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t2" 
+  and     a2: "s1\<longrightarrow>\<^sub>\<beta>\<^sup>*s2" 
+  shows "App t1 s1\<longrightarrow>\<^sub>\<beta>\<^sup>* App t2 s2"
 proof -
-  have "App t1 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s1" using a1 by (rule one_app_congL)
+  have "App t1 s1 \<longrightarrow>\<^sub>\<beta>\<^sup>* App t2 s1" using a1 by (rule one_app_congL)
   moreover
-  have "App t2 s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App t2 s2" using a2 by (rule one_app_congR)
+  have "App t2 s1 \<longrightarrow>\<^sub>\<beta>\<^sup>* App t2 s2" using a2 by (rule one_app_congR)
   ultimately show ?thesis by (rule beta_star_trans)
 qed
 
 lemma one_beta_star: 
-  assumes a: "(t1\<longrightarrow>\<^isub>1t2)" 
-  shows "(t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2)"
+  assumes a: "(t1\<longrightarrow>\<^sub>1t2)" 
+  shows "(t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t2)"
   using a
 proof(nominal_induct rule: One.strong_induct)
   case o1 thus ?case by simp
@@ -519,16 +519,16 @@
 next 
   case (o4 a s1 s2 t1 t2)
   have vc: "a\<sharp>s1" "a\<sharp>s2" by fact+
-  have a1: "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^isub>\<beta>\<^sup>*s2" by fact+
-  have c1: "(App (Lam [a].t2) s2) \<longrightarrow>\<^isub>\<beta> (t2 [a::= s2])" using vc by (simp add: b4)
-  from a1 a2 have c2: "App (Lam [a].t1 ) s1 \<longrightarrow>\<^isub>\<beta>\<^sup>* App (Lam [a].t2 ) s2" 
+  have a1: "t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t2" and a2: "s1\<longrightarrow>\<^sub>\<beta>\<^sup>*s2" by fact+
+  have c1: "(App (Lam [a].t2) s2) \<longrightarrow>\<^sub>\<beta> (t2 [a::= s2])" using vc by (simp add: b4)
+  from a1 a2 have c2: "App (Lam [a].t1 ) s1 \<longrightarrow>\<^sub>\<beta>\<^sup>* App (Lam [a].t2 ) s2" 
     by (blast intro!: one_app_cong one_lam_cong)
   show ?case using c2 c1 by (blast intro: beta_star_trans)
 qed
  
 lemma one_star_lam_cong: 
-  assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" 
-  shows "(Lam  [a].t1)\<longrightarrow>\<^isub>1\<^sup>* (Lam [a].t2)"
+  assumes a: "t1\<longrightarrow>\<^sub>1\<^sup>*t2" 
+  shows "(Lam  [a].t1)\<longrightarrow>\<^sub>1\<^sup>* (Lam [a].t2)"
   using a
 proof induct
   case os1 thus ?case by simp
@@ -537,8 +537,8 @@
 qed
 
 lemma one_star_app_congL: 
-  assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" 
-  shows "App t1 s\<longrightarrow>\<^isub>1\<^sup>* App t2 s"
+  assumes a: "t1\<longrightarrow>\<^sub>1\<^sup>*t2" 
+  shows "App t1 s\<longrightarrow>\<^sub>1\<^sup>* App t2 s"
   using a
 proof induct
   case os1 thus ?case by simp
@@ -547,8 +547,8 @@
 qed
 
 lemma one_star_app_congR: 
-  assumes a: "t1\<longrightarrow>\<^isub>1\<^sup>*t2" 
-  shows "App s t1 \<longrightarrow>\<^isub>1\<^sup>* App s t2"
+  assumes a: "t1\<longrightarrow>\<^sub>1\<^sup>*t2" 
+  shows "App s t1 \<longrightarrow>\<^sub>1\<^sup>* App s t2"
   using a
 proof induct
   case os1 thus ?case by simp
@@ -557,8 +557,8 @@
 qed
 
 lemma beta_one_star: 
-  assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2" 
-  shows "t1\<longrightarrow>\<^isub>1\<^sup>*t2"
+  assumes a: "t1\<longrightarrow>\<^sub>\<beta>t2" 
+  shows "t1\<longrightarrow>\<^sub>1\<^sup>*t2"
   using a
 proof(induct)
   case b1 thus ?case by (blast intro!: one_star_app_congL)
@@ -571,88 +571,88 @@
 qed
 
 lemma trans_closure: 
-  shows "(M1\<longrightarrow>\<^isub>1\<^sup>*M2) = (M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2)"
+  shows "(M1\<longrightarrow>\<^sub>1\<^sup>*M2) = (M1\<longrightarrow>\<^sub>\<beta>\<^sup>*M2)"
 proof
-  assume "M1 \<longrightarrow>\<^isub>1\<^sup>* M2"
-  then show "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2"
+  assume "M1 \<longrightarrow>\<^sub>1\<^sup>* M2"
+  then show "M1\<longrightarrow>\<^sub>\<beta>\<^sup>*M2"
   proof induct
-    case (os1 M1) thus "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M1" by simp
+    case (os1 M1) thus "M1\<longrightarrow>\<^sub>\<beta>\<^sup>*M1" by simp
   next
     case (os2 M1 M2 M3)
-    have "M2\<longrightarrow>\<^isub>1M3" by fact
-    then have "M2\<longrightarrow>\<^isub>\<beta>\<^sup>*M3" by (rule one_beta_star)
-    moreover have "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M2" by fact
-    ultimately show "M1\<longrightarrow>\<^isub>\<beta>\<^sup>*M3" by (auto intro: beta_star_trans)
+    have "M2\<longrightarrow>\<^sub>1M3" by fact
+    then have "M2\<longrightarrow>\<^sub>\<beta>\<^sup>*M3" by (rule one_beta_star)
+    moreover have "M1\<longrightarrow>\<^sub>\<beta>\<^sup>*M2" by fact
+    ultimately show "M1\<longrightarrow>\<^sub>\<beta>\<^sup>*M3" by (auto intro: beta_star_trans)
   qed
 next
-  assume "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M2" 
-  then show "M1\<longrightarrow>\<^isub>1\<^sup>*M2"
+  assume "M1 \<longrightarrow>\<^sub>\<beta>\<^sup>* M2" 
+  then show "M1\<longrightarrow>\<^sub>1\<^sup>*M2"
   proof induct
-    case (bs1 M1) thus  "M1\<longrightarrow>\<^isub>1\<^sup>*M1" by simp
+    case (bs1 M1) thus  "M1\<longrightarrow>\<^sub>1\<^sup>*M1" by simp
   next
     case (bs2 M1 M2 M3) 
-    have "M2\<longrightarrow>\<^isub>\<beta>M3" by fact
-    then have "M2\<longrightarrow>\<^isub>1\<^sup>*M3" by (rule beta_one_star)
-    moreover have "M1\<longrightarrow>\<^isub>1\<^sup>*M2" by fact
-    ultimately show "M1\<longrightarrow>\<^isub>1\<^sup>*M3" by (auto intro: one_star_trans)
+    have "M2\<longrightarrow>\<^sub>\<beta>M3" by fact
+    then have "M2\<longrightarrow>\<^sub>1\<^sup>*M3" by (rule beta_one_star)
+    moreover have "M1\<longrightarrow>\<^sub>1\<^sup>*M2" by fact
+    ultimately show "M1\<longrightarrow>\<^sub>1\<^sup>*M3" by (auto intro: one_star_trans)
   qed
 qed
 
 lemma cr_one:
-  assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t1" 
-  and     b: "t\<longrightarrow>\<^isub>1t2"
-  shows "\<exists>t3. t1\<longrightarrow>\<^isub>1t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3"
+  assumes a: "t\<longrightarrow>\<^sub>1\<^sup>*t1" 
+  and     b: "t\<longrightarrow>\<^sub>1t2"
+  shows "\<exists>t3. t1\<longrightarrow>\<^sub>1t3 \<and> t2\<longrightarrow>\<^sub>1\<^sup>*t3"
   using a b
 proof (induct arbitrary: t2)
   case os1 thus ?case by force
 next
   case (os2 t s1 s2 t2)  
-  have b: "s1 \<longrightarrow>\<^isub>1 s2" by fact
-  have h: "\<And>t2. t \<longrightarrow>\<^isub>1 t2 \<Longrightarrow> (\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3)" by fact
-  have c: "t \<longrightarrow>\<^isub>1 t2" by fact
-  show "\<exists>t3. s2 \<longrightarrow>\<^isub>1 t3 \<and>  t2 \<longrightarrow>\<^isub>1\<^sup>* t3" 
+  have b: "s1 \<longrightarrow>\<^sub>1 s2" by fact
+  have h: "\<And>t2. t \<longrightarrow>\<^sub>1 t2 \<Longrightarrow> (\<exists>t3. s1 \<longrightarrow>\<^sub>1 t3 \<and> t2 \<longrightarrow>\<^sub>1\<^sup>* t3)" by fact
+  have c: "t \<longrightarrow>\<^sub>1 t2" by fact
+  show "\<exists>t3. s2 \<longrightarrow>\<^sub>1 t3 \<and>  t2 \<longrightarrow>\<^sub>1\<^sup>* t3" 
   proof -
-    from c h have "\<exists>t3. s1 \<longrightarrow>\<^isub>1 t3 \<and> t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast
-    then obtain t3 where c1: "s1 \<longrightarrow>\<^isub>1 t3" and c2: "t2 \<longrightarrow>\<^isub>1\<^sup>* t3" by blast
-    have "\<exists>t4. s2 \<longrightarrow>\<^isub>1 t4 \<and> t3 \<longrightarrow>\<^isub>1 t4" using b c1 by (blast intro: diamond)
+    from c h have "\<exists>t3. s1 \<longrightarrow>\<^sub>1 t3 \<and> t2 \<longrightarrow>\<^sub>1\<^sup>* t3" by blast
+    then obtain t3 where c1: "s1 \<longrightarrow>\<^sub>1 t3" and c2: "t2 \<longrightarrow>\<^sub>1\<^sup>* t3" by blast
+    have "\<exists>t4. s2 \<longrightarrow>\<^sub>1 t4 \<and> t3 \<longrightarrow>\<^sub>1 t4" using b c1 by (blast intro: diamond)
     thus ?thesis using c2 by (blast intro: one_star_trans)
   qed
 qed
 
 lemma cr_one_star: 
-  assumes a: "t\<longrightarrow>\<^isub>1\<^sup>*t2"
-      and b: "t\<longrightarrow>\<^isub>1\<^sup>*t1"
-    shows "\<exists>t3. t1\<longrightarrow>\<^isub>1\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>1\<^sup>*t3"
+  assumes a: "t\<longrightarrow>\<^sub>1\<^sup>*t2"
+      and b: "t\<longrightarrow>\<^sub>1\<^sup>*t1"
+    shows "\<exists>t3. t1\<longrightarrow>\<^sub>1\<^sup>*t3\<and>t2\<longrightarrow>\<^sub>1\<^sup>*t3"
 using a b
 proof (induct arbitrary: t1)
   case (os1 t) then show ?case by force
 next 
   case (os2 t s1 s2 t1)
-  have c: "t \<longrightarrow>\<^isub>1\<^sup>* s1" by fact
-  have c': "t \<longrightarrow>\<^isub>1\<^sup>* t1" by fact
-  have d: "s1 \<longrightarrow>\<^isub>1 s2" by fact
-  have "t \<longrightarrow>\<^isub>1\<^sup>* t1 \<Longrightarrow> (\<exists>t3.  t1 \<longrightarrow>\<^isub>1\<^sup>* t3 \<and> s1 \<longrightarrow>\<^isub>1\<^sup>* t3)" by fact
-  then obtain t3 where f1: "t1 \<longrightarrow>\<^isub>1\<^sup>* t3"
-                   and f2: "s1 \<longrightarrow>\<^isub>1\<^sup>* t3" using c' by blast
-  from cr_one d f2 have "\<exists>t4. t3\<longrightarrow>\<^isub>1t4 \<and> s2\<longrightarrow>\<^isub>1\<^sup>*t4" by blast
-  then obtain t4 where g1: "t3\<longrightarrow>\<^isub>1t4"
-                   and g2: "s2\<longrightarrow>\<^isub>1\<^sup>*t4" by blast
-  have "t1\<longrightarrow>\<^isub>1\<^sup>*t4" using f1 g1 by (blast intro: one_star_trans)
+  have c: "t \<longrightarrow>\<^sub>1\<^sup>* s1" by fact
+  have c': "t \<longrightarrow>\<^sub>1\<^sup>* t1" by fact
+  have d: "s1 \<longrightarrow>\<^sub>1 s2" by fact
+  have "t \<longrightarrow>\<^sub>1\<^sup>* t1 \<Longrightarrow> (\<exists>t3.  t1 \<longrightarrow>\<^sub>1\<^sup>* t3 \<and> s1 \<longrightarrow>\<^sub>1\<^sup>* t3)" by fact
+  then obtain t3 where f1: "t1 \<longrightarrow>\<^sub>1\<^sup>* t3"
+                   and f2: "s1 \<longrightarrow>\<^sub>1\<^sup>* t3" using c' by blast
+  from cr_one d f2 have "\<exists>t4. t3\<longrightarrow>\<^sub>1t4 \<and> s2\<longrightarrow>\<^sub>1\<^sup>*t4" by blast
+  then obtain t4 where g1: "t3\<longrightarrow>\<^sub>1t4"
+                   and g2: "s2\<longrightarrow>\<^sub>1\<^sup>*t4" by blast
+  have "t1\<longrightarrow>\<^sub>1\<^sup>*t4" using f1 g1 by (blast intro: one_star_trans)
   thus ?case using g2 by blast
 qed
   
 lemma cr_beta_star: 
-  assumes a1: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t1" 
-  and     a2: "t\<longrightarrow>\<^isub>\<beta>\<^sup>*t2" 
-  shows "\<exists>t3. t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3"
+  assumes a1: "t\<longrightarrow>\<^sub>\<beta>\<^sup>*t1" 
+  and     a2: "t\<longrightarrow>\<^sub>\<beta>\<^sup>*t2" 
+  shows "\<exists>t3. t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^sub>\<beta>\<^sup>*t3"
 proof -
-  from a1 have "t\<longrightarrow>\<^isub>1\<^sup>*t1" by (simp only: trans_closure)
+  from a1 have "t\<longrightarrow>\<^sub>1\<^sup>*t1" by (simp only: trans_closure)
   moreover
-  from a2 have "t\<longrightarrow>\<^isub>1\<^sup>*t2" by (simp only: trans_closure)
-  ultimately have "\<exists>t3. t1\<longrightarrow>\<^isub>1\<^sup>*t3 \<and> t2\<longrightarrow>\<^isub>1\<^sup>*t3" by (blast intro: cr_one_star) 
-  then obtain t3 where "t1\<longrightarrow>\<^isub>1\<^sup>*t3" and "t2\<longrightarrow>\<^isub>1\<^sup>*t3" by blast
-  hence "t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" and "t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" by (simp_all only: trans_closure)
-  then show "\<exists>t3. t1\<longrightarrow>\<^isub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^isub>\<beta>\<^sup>*t3" by blast
+  from a2 have "t\<longrightarrow>\<^sub>1\<^sup>*t2" by (simp only: trans_closure)
+  ultimately have "\<exists>t3. t1\<longrightarrow>\<^sub>1\<^sup>*t3 \<and> t2\<longrightarrow>\<^sub>1\<^sup>*t3" by (blast intro: cr_one_star) 
+  then obtain t3 where "t1\<longrightarrow>\<^sub>1\<^sup>*t3" and "t2\<longrightarrow>\<^sub>1\<^sup>*t3" by blast
+  hence "t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t3" and "t2\<longrightarrow>\<^sub>\<beta>\<^sup>*t3" by (simp_all only: trans_closure)
+  then show "\<exists>t3. t1\<longrightarrow>\<^sub>\<beta>\<^sup>*t3\<and>t2\<longrightarrow>\<^sub>\<beta>\<^sup>*t3" by blast
 qed
 
 end