# HG changeset patch
# User wenzelm
# Date 1354114758 -3600
# Node ID 4aa34bd43228519583bb834341a84142a660c17d
# Parent  227477f17c26397c62e3fbbb7c0a57957bd2f03e
eliminated slightly odd identifiers;

diff -r 227477f17c26 -r 4aa34bd43228 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Wed Nov 28 15:38:12 2012 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Nov 28 15:59:18 2012 +0100
@@ -1004,7 +1004,7 @@
   plusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of +\<infinity>*)
   minusinf:: "fm \<Rightarrow> fm" (* Virtual substitution of -\<infinity>*)
   \<delta> :: "fm \<Rightarrow> int" (* Compute lcm {d| N\<^isup>? Dvd c*x+t \<in> p}*)
-  d\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* checks if a given l divides all the ds above*)
+  d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* checks if a given l divides all the ds above*)
 
 recdef minusinf "measure size"
   "minusinf (And p q) = And (minusinf p) (minusinf q)" 
@@ -1038,18 +1038,18 @@
   "\<delta> (NDvd i (CN 0 c e)) = i"
   "\<delta> p = 1"
 
-recdef d\<delta> "measure size"
-  "d\<delta> (And p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" 
-  "d\<delta> (Or p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" 
-  "d\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
-  "d\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
-  "d\<delta> p = (\<lambda> d. True)"
+recdef d_\<delta> "measure size"
+  "d_\<delta> (And p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)" 
+  "d_\<delta> (Or p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)" 
+  "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
+  "d_\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
+  "d_\<delta> p = (\<lambda> d. True)"
 
 lemma delta_mono: 
   assumes lin: "iszlfm p"
   and d: "d dvd d'"
-  and ad: "d\<delta> p d"
-  shows "d\<delta> p d'"
+  and ad: "d_\<delta> p d"
+  shows "d_\<delta> p d'"
   using lin ad d
 proof(induct p rule: iszlfm.induct)
   case (9 i c e)  thus ?case using d
@@ -1060,61 +1060,61 @@
 qed simp_all
 
 lemma \<delta> : assumes lin:"iszlfm p"
-  shows "d\<delta> p (\<delta> p) \<and> \<delta> p >0"
+  shows "d_\<delta> p (\<delta> p) \<and> \<delta> p >0"
 using lin
 proof (induct p rule: iszlfm.induct)
   case (1 p q) 
   let ?d = "\<delta> (And p q)"
   from 1 lcm_pos_int have dp: "?d >0" by simp
   have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp
-  hence th: "d\<delta> p ?d" using delta_mono 1(2,3) by(simp only: iszlfm.simps)
+  hence th: "d_\<delta> p ?d" using delta_mono 1(2,3) by(simp only: iszlfm.simps)
   have "\<delta> q dvd \<delta> (And p q)" using 1 by simp
-  hence th': "d\<delta> q ?d" using delta_mono 1 by(simp only: iszlfm.simps)
+  hence th': "d_\<delta> q ?d" using delta_mono 1 by(simp only: iszlfm.simps)
   from th th' dp show ?case by simp
 next
   case (2 p q)  
   let ?d = "\<delta> (And p q)"
   from 2 lcm_pos_int have dp: "?d >0" by simp
   have "\<delta> p dvd \<delta> (And p q)" using 2 by simp
-  hence th: "d\<delta> p ?d" using delta_mono 2 by(simp only: iszlfm.simps)
+  hence th: "d_\<delta> p ?d" using delta_mono 2 by(simp only: iszlfm.simps)
   have "\<delta> q dvd \<delta> (And p q)" using 2 by simp
-  hence th': "d\<delta> q ?d" using delta_mono 2 by(simp only: iszlfm.simps)
+  hence th': "d_\<delta> q ?d" using delta_mono 2 by(simp only: iszlfm.simps)
   from th th' dp show ?case by simp
 qed simp_all
 
 
 consts 
-  a\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
-  d\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
+  a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
+  d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
   \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
   \<beta> :: "fm \<Rightarrow> num list"
   \<alpha> :: "fm \<Rightarrow> num list"
 
-recdef a\<beta> "measure size"
-  "a\<beta> (And p q) = (\<lambda> k. And (a\<beta> p k) (a\<beta> q k))" 
-  "a\<beta> (Or p q) = (\<lambda> k. Or (a\<beta> p k) (a\<beta> q k))" 
-  "a\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> p = (\<lambda> k. p)"
+recdef a_\<beta> "measure size"
+  "a_\<beta> (And p q) = (\<lambda> k. And (a_\<beta> p k) (a_\<beta> q k))" 
+  "a_\<beta> (Or p q) = (\<lambda> k. Or (a_\<beta> p k) (a_\<beta> q k))" 
+  "a_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> p = (\<lambda> k. p)"
 
-recdef d\<beta> "measure size"
-  "d\<beta> (And p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))" 
-  "d\<beta> (Or p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))" 
-  "d\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
-  "d\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
-  "d\<beta> p = (\<lambda> k. True)"
+recdef d_\<beta> "measure size"
+  "d_\<beta> (And p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))" 
+  "d_\<beta> (Or p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))" 
+  "d_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
+  "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
+  "d_\<beta> p = (\<lambda> k. True)"
 
 recdef \<zeta> "measure size"
   "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)" 
@@ -1169,7 +1169,7 @@
 
 lemma minusinf_inf:
   assumes linp: "iszlfm p"
-  and u: "d\<beta> p 1"
+  and u: "d_\<beta> p 1"
   shows "\<exists> (z::int). \<forall> x < z. Ifm bbs (x#bs) (minusinf p) = Ifm bbs (x#bs) p"
   (is "?P p" is "\<exists> (z::int). \<forall> x < z. ?I x (?M p) = ?I x p")
 using linp u
@@ -1242,7 +1242,7 @@
 qed auto
 
 lemma minusinf_repeats:
-  assumes d: "d\<delta> p d" and linp: "iszlfm p"
+  assumes d: "d_\<delta> p d" and linp: "iszlfm p"
   shows "Ifm bbs ((x - k*d)#bs) (minusinf p) = Ifm bbs (x #bs) (minusinf p)"
 using linp d
 proof(induct p rule: iszlfm.induct) 
@@ -1301,7 +1301,7 @@
     qed
 qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="x - k*d" and b'="x"])
 
-lemma mirror\<alpha>\<beta>:
+lemma mirror_\<alpha>_\<beta>:
   assumes lp: "iszlfm p"
   shows "(Inum (i#bs)) ` set (\<alpha> p) = (Inum (i#bs)) ` set (\<beta> (mirror p))"
 using lp
@@ -1337,8 +1337,8 @@
   finally show ?case by simp
 qed (auto simp add: numbound0_I[where bs="bs" and b="x" and b'="- x"] gr0_conv_Suc)
 
-lemma mirror_l: "iszlfm p \<and> d\<beta> p 1 
-  \<Longrightarrow> iszlfm (mirror p) \<and> d\<beta> (mirror p) 1"
+lemma mirror_l: "iszlfm p \<and> d_\<beta> p 1 
+  \<Longrightarrow> iszlfm (mirror p) \<and> d_\<beta> (mirror p) 1"
   by (induct p rule: mirror.induct) auto
 
 lemma mirror_\<delta>: "iszlfm p \<Longrightarrow> \<delta> (mirror p) = \<delta> p"
@@ -1348,11 +1348,11 @@
   shows "\<forall> b\<in> set (\<beta> p). numbound0 b"
   using lp by (induct p rule: \<beta>.induct) auto
 
-lemma d\<beta>_mono: 
+lemma d_\<beta>_mono: 
   assumes linp: "iszlfm p"
-  and dr: "d\<beta> p l"
+  and dr: "d_\<beta> p l"
   and d: "l dvd l'"
-  shows "d\<beta> p l'"
+  shows "d_\<beta> p l'"
 using dr linp dvd_trans[of _ "l" "l'", simplified d]
   by (induct p rule: iszlfm.induct) simp_all
 
@@ -1363,26 +1363,26 @@
 
 lemma \<zeta>: 
   assumes linp: "iszlfm p"
-  shows "\<zeta> p > 0 \<and> d\<beta> p (\<zeta> p)"
+  shows "\<zeta> p > 0 \<and> d_\<beta> p (\<zeta> p)"
 using linp
 proof(induct p rule: iszlfm.induct)
   case (1 p q)
   from 1 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
-  from 1 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
-    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
+  from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
+    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
     dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
 next
   case (2 p q)
   from 2 have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
-  from 2 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
-    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
+  from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
+    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
     dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
 qed (auto simp add: lcm_pos_int)
 
-lemma a\<beta>: assumes linp: "iszlfm p" and d: "d\<beta> p l" and lp: "l > 0"
-  shows "iszlfm (a\<beta> p l) \<and> d\<beta> (a\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a\<beta> p l) = Ifm bbs (x#bs) p)"
+lemma a_\<beta>: assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l > 0"
+  shows "iszlfm (a_\<beta> p l) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> (Ifm bbs (l*x #bs) (a_\<beta> p l) = Ifm bbs (x#bs) p)"
 using linp d
 proof (induct p rule: iszlfm.induct)
   case (5 c e) hence cp: "c>0" and be: "numbound0 e" and d': "c dvd l" by simp+
@@ -1530,20 +1530,20 @@
   finally show ?case using numbound0_I[OF be,where b="(l * x)" and b'="x" and bs="bs"] be  mult_strict_mono[OF ldcp jp ldcp ] by (simp add: dvd_def)
 qed (auto simp add: gr0_conv_Suc numbound0_I[where bs="bs" and b="(l * x)" and b'="x"])
 
-lemma a\<beta>_ex: assumes linp: "iszlfm p" and d: "d\<beta> p l" and lp: "l>0"
-  shows "(\<exists> x. l dvd x \<and> Ifm bbs (x #bs) (a\<beta> p l)) = (\<exists> (x::int). Ifm bbs (x#bs) p)"
+lemma a_\<beta>_ex: assumes linp: "iszlfm p" and d: "d_\<beta> p l" and lp: "l>0"
+  shows "(\<exists> x. l dvd x \<and> Ifm bbs (x #bs) (a_\<beta> p l)) = (\<exists> (x::int). Ifm bbs (x#bs) p)"
   (is "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> x. ?P' x)")
 proof-
   have "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> (x::int). ?P (l*x))"
     using unity_coeff_ex[where l="l" and P="?P", simplified] by simp
-  also have "\<dots> = (\<exists> (x::int). ?P' x)" using a\<beta>[OF linp d lp] by simp
+  also have "\<dots> = (\<exists> (x::int). ?P' x)" using a_\<beta>[OF linp d lp] by simp
   finally show ?thesis  . 
 qed
 
 lemma \<beta>:
   assumes lp: "iszlfm p"
-  and u: "d\<beta> p 1"
-  and d: "d\<delta> p d"
+  and u: "d_\<beta> p 1"
+  and d: "d_\<delta> p d"
   and dp: "d > 0"
   and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). x = b + j)"
   and p: "Ifm bbs (x#bs) p" (is "?P x")
@@ -1637,8 +1637,8 @@
 
 lemma \<beta>':   
   assumes lp: "iszlfm p"
-  and u: "d\<beta> p 1"
-  and d: "d\<delta> p d"
+  and u: "d_\<beta> p 1"
+  and d: "d_\<delta> p d"
   and dp: "d > 0"
   shows "\<forall> x. \<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> set(\<beta> p). Ifm bbs ((Inum (a#bs) b + j) #bs) p) \<longrightarrow> Ifm bbs (x#bs) p \<longrightarrow> Ifm bbs ((x - d)#bs) p" (is "\<forall> x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
 proof(clarify)
@@ -1672,8 +1672,8 @@
 
 theorem cp_thm:
   assumes lp: "iszlfm p"
-  and u: "d\<beta> p 1"
-  and d: "d\<delta> p d"
+  and u: "d_\<beta> p 1"
+  and d: "d_\<delta> p d"
   and dp: "d > 0"
   shows "(\<exists> (x::int). Ifm bbs (x #bs) p) = (\<exists> j\<in> {1.. d}. Ifm bbs (j #bs) (minusinf p) \<or> (\<exists> b \<in> set (\<beta> p). Ifm bbs ((Inum (i#bs) b + j) #bs) p))"
   (is "(\<exists> (x::int). ?P (x)) = (\<exists> j\<in> ?D. ?M j \<or> (\<exists> b\<in> ?B. ?P (?I b + j)))")
@@ -1706,27 +1706,27 @@
 
 lemma cp_thm': 
   assumes lp: "iszlfm p"
-  and up: "d\<beta> p 1" and dd: "d\<delta> p d" and dp: "d > 0"
+  and up: "d_\<beta> p 1" and dd: "d_\<delta> p d" and dp: "d > 0"
   shows "(\<exists> x. Ifm bbs (x#bs) p) = ((\<exists> j\<in> {1 .. d}. Ifm bbs (j#bs) (minusinf p)) \<or> (\<exists> j\<in> {1.. d}. \<exists> b\<in> (Inum (i#bs)) ` set (\<beta> p). Ifm bbs ((b+j)#bs) p))"
   using cp_thm[OF lp up dd dp,where i="i"] by auto
 
 definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int" where
-  "unit p \<equiv> (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a\<beta> p' l); d = \<delta> q;
+  "unit p \<equiv> (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l); d = \<delta> q;
              B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q))
              in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"
 
 lemma unit: assumes qf: "qfree p"
-  shows "\<And> q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists> x. Ifm bbs (x#bs) p) = (\<exists> x. Ifm bbs (x#bs) q)) \<and> (Inum (i#bs)) ` set B = (Inum (i#bs)) ` set (\<beta> q) \<and> d\<beta> q 1 \<and> d\<delta> q d \<and> d >0 \<and> iszlfm q \<and> (\<forall> b\<in> set B. numbound0 b)"
+  shows "\<And> q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists> x. Ifm bbs (x#bs) p) = (\<exists> x. Ifm bbs (x#bs) q)) \<and> (Inum (i#bs)) ` set B = (Inum (i#bs)) ` set (\<beta> q) \<and> d_\<beta> q 1 \<and> d_\<delta> q d \<and> d >0 \<and> iszlfm q \<and> (\<forall> b\<in> set B. numbound0 b)"
 proof-
   fix q B d 
   assume qBd: "unit p = (q,B,d)"
   let ?thes = "((\<exists> x. Ifm bbs (x#bs) p) = (\<exists> x. Ifm bbs (x#bs) q)) \<and>
     Inum (i#bs) ` set B = Inum (i#bs) ` set (\<beta> q) \<and>
-    d\<beta> q 1 \<and> d\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall> b\<in> set B. numbound0 b)"
+    d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q \<and> (\<forall> b\<in> set B. numbound0 b)"
   let ?I = "\<lambda> x p. Ifm bbs (x#bs) p"
   let ?p' = "zlfm p"
   let ?l = "\<zeta> ?p'"
-  let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a\<beta> ?p' ?l)"
+  let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a_\<beta> ?p' ?l)"
   let ?d = "\<delta> ?q"
   let ?B = "set (\<beta> ?q)"
   let ?B'= "remdups (map simpnum (\<beta> ?q))"
@@ -1736,11 +1736,11 @@
   have pp': "\<forall> i. ?I i ?p' = ?I i p" by auto
   from conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]]
   have lp': "iszlfm ?p'" . 
-  from lp' \<zeta>[where p="?p'"] have lp: "?l >0" and dl: "d\<beta> ?p' ?l" by auto
-  from a\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp' dl lp] pp'
+  from lp' \<zeta>[where p="?p'"] have lp: "?l >0" and dl: "d_\<beta> ?p' ?l" by auto
+  from a_\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp' dl lp] pp'
   have pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by simp 
-  from lp' lp a\<beta>[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d\<beta> ?q 1"  by auto
-  from \<delta>[OF lq] have dp:"?d >0" and dd: "d\<delta> ?q ?d" by blast+
+  from lp' lp a_\<beta>[OF lp' dl lp] have lq:"iszlfm ?q" and uq: "d_\<beta> ?q 1"  by auto
+  from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+
   let ?N = "\<lambda> t. Inum (i#bs) t"
   have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by auto 
   also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="i#bs"] by auto
@@ -1762,13 +1762,13 @@
   {assume "\<not> (length ?B' \<le> length ?A')"
     hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
       using qBd by (auto simp add: Let_def unit_def)
-    with AA' mirror\<alpha>\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)" 
+    with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)" 
       and bn: "\<forall>b\<in> set B. numbound0 b" by simp+
     from mirror_ex[OF lq] pq_ex q 
     have pqm_eq:"(\<exists> (x::int). ?I x p) = (\<exists> (x::int). ?I x q)" by simp
     from lq uq q mirror_l[where p="?q"]
-    have lq': "iszlfm q" and uq: "d\<beta> q 1" by auto
-    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d\<delta> q d " by auto
+    have lq': "iszlfm q" and uq: "d_\<beta> q 1" by auto
+    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d_\<delta> q d " by auto
     from pqm_eq b bn uq lq' dp dq q dp d have ?thes by simp
   }
   ultimately show ?thes by blast
@@ -1803,7 +1803,7 @@
   have qbf:"unit p = (?q,?B,?d)" by simp
   from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists> (x::int). ?I x ?q)" and 
     B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and 
-    uq:"d\<beta> ?q 1" and dd: "d\<delta> ?q ?d" and dp: "?d > 0" and 
+    uq:"d_\<beta> ?q 1" and dd: "d_\<delta> ?q ?d" and dp: "?d > 0" and 
     lq: "iszlfm ?q" and 
     Bn: "\<forall> b\<in> set ?B. numbound0 b" by auto
   from zlin_qfree[OF lq] have qfq: "qfree ?q" .
diff -r 227477f17c26 -r 4aa34bd43228 src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Wed Nov 28 15:38:12 2012 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy	Wed Nov 28 15:59:18 2012 +0100
@@ -1947,7 +1947,7 @@
 text{* plusinf : Virtual substitution of @{text "+\<infinity>"}
        minusinf: Virtual substitution of @{text "-\<infinity>"}
        @{text "\<delta>"} Compute lcm @{text "d| Dvd d  c*x+t \<in> p"}
-       @{text "d\<delta>"} checks if a given l divides all the ds above*}
+       @{text "d_\<delta>"} checks if a given l divides all the ds above*}
 
 fun minusinf:: "fm \<Rightarrow> fm" where
   "minusinf (And p q) = conj (minusinf p) (minusinf q)" 
@@ -1981,18 +1981,18 @@
 | "\<delta> (NDvd i (CN 0 c e)) = i"
 | "\<delta> p = 1"
 
-fun d\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" where
-  "d\<delta> (And p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" 
-| "d\<delta> (Or p q) = (\<lambda> d. d\<delta> p d \<and> d\<delta> q d)" 
-| "d\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
-| "d\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
-| "d\<delta> p = (\<lambda> d. True)"
+fun d_\<delta> :: "fm \<Rightarrow> int \<Rightarrow> bool" where
+  "d_\<delta> (And p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)" 
+| "d_\<delta> (Or p q) = (\<lambda> d. d_\<delta> p d \<and> d_\<delta> q d)" 
+| "d_\<delta> (Dvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
+| "d_\<delta> (NDvd i (CN 0 c e)) = (\<lambda> d. i dvd d)"
+| "d_\<delta> p = (\<lambda> d. True)"
 
 lemma delta_mono: 
   assumes lin: "iszlfm p bs"
   and d: "d dvd d'"
-  and ad: "d\<delta> p d"
-  shows "d\<delta> p d'"
+  and ad: "d_\<delta> p d"
+  shows "d_\<delta> p d'"
   using lin ad d
 proof(induct p rule: iszlfm.induct)
   case (9 i c e)  thus ?case using d
@@ -2003,26 +2003,26 @@
 qed simp_all
 
 lemma \<delta> : assumes lin:"iszlfm p bs"
-  shows "d\<delta> p (\<delta> p) \<and> \<delta> p >0"
+  shows "d_\<delta> p (\<delta> p) \<and> \<delta> p >0"
 using lin
 proof (induct p rule: iszlfm.induct)
   case (1 p q) 
   let ?d = "\<delta> (And p q)"
   from 1 lcm_pos_int have dp: "?d >0" by simp
   have d1: "\<delta> p dvd \<delta> (And p q)" using 1 by simp 
-  hence th: "d\<delta> p ?d" 
+  hence th: "d_\<delta> p ?d" 
     using delta_mono 1 by (simp only: iszlfm.simps) blast
   have "\<delta> q dvd \<delta> (And p q)" using 1 by simp 
-  hence th': "d\<delta> q ?d" using delta_mono 1 by (simp only: iszlfm.simps) blast
+  hence th': "d_\<delta> q ?d" using delta_mono 1 by (simp only: iszlfm.simps) blast
   from th th' dp show ?case by simp 
 next
   case (2 p q)  
   let ?d = "\<delta> (And p q)"
   from 2 lcm_pos_int have dp: "?d >0" by simp
   have "\<delta> p dvd \<delta> (And p q)" using 2 by simp
-  hence th: "d\<delta> p ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
+  hence th: "d_\<delta> p ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
   have "\<delta> q dvd \<delta> (And p q)" using 2 by simp
-  hence th': "d\<delta> q ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
+  hence th': "d_\<delta> q ?d" using delta_mono 2 by (simp only: iszlfm.simps) blast
   from th th' dp show ?case by simp
 qed simp_all
 
@@ -2152,7 +2152,7 @@
 qed simp_all
 
 lemma minusinf_repeats:
-  assumes d: "d\<delta> p d" and linp: "iszlfm p (a # bs)"
+  assumes d: "d_\<delta> p d" and linp: "iszlfm p (a # bs)"
   shows "Ifm ((real(x - k*d))#bs) (minusinf p) = Ifm (real x #bs) (minusinf p)"
 using linp d
 proof(induct p rule: iszlfm.induct) 
@@ -2218,7 +2218,7 @@
 proof-
   let ?d = "\<delta> p"
   from \<delta> [OF lin] have dpos: "?d >0" by simp
-  from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
+  from \<delta> [OF lin] have alld: "d_\<delta> p ?d" by simp
   from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P1 x = ?P1 (x - (k * ?d))" by simp
   from minusinf_inf[OF lin] have th2:"\<exists> z. \<forall> x. x<z \<longrightarrow> (?P x = ?P1 x)" by blast
   from minusinfinity [OF dpos th1 th2] exmi show ?thesis by blast
@@ -2232,7 +2232,7 @@
 proof-
   let ?d = "\<delta> p"
   from \<delta> [OF lin] have dpos: "?d >0" by simp
-  from \<delta> [OF lin] have alld: "d\<delta> p ?d" by simp
+  from \<delta> [OF lin] have alld: "d_\<delta> p ?d" by simp
   from minusinf_repeats[OF alld lin] have th1:"\<forall> x k. ?P x = ?P (x - (k * ?d))" by simp
   from periodic_finite_ex[OF dpos th1] show ?thesis by blast
 qed
@@ -2240,37 +2240,37 @@
 lemma dvd1_eq1: "x >0 \<Longrightarrow> (x::int) dvd 1 = (x = 1)" by auto
 
 consts 
-  a\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
-  d\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
+  a_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> fm" (* adjusts the coeffitients of a formula *)
+  d_\<beta> :: "fm \<Rightarrow> int \<Rightarrow> bool" (* tests if all coeffs c of c divide a given l*)
   \<zeta>  :: "fm \<Rightarrow> int" (* computes the lcm of all coefficients of x*)
   \<beta> :: "fm \<Rightarrow> num list"
   \<alpha> :: "fm \<Rightarrow> num list"
 
-recdef a\<beta> "measure size"
-  "a\<beta> (And p q) = (\<lambda> k. And (a\<beta> p k) (a\<beta> q k))" 
-  "a\<beta> (Or p q) = (\<lambda> k. Or (a\<beta> p k) (a\<beta> q k))" 
-  "a\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
-  "a\<beta> p = (\<lambda> k. p)"
-
-recdef d\<beta> "measure size"
-  "d\<beta> (And p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))" 
-  "d\<beta> (Or p q) = (\<lambda> k. (d\<beta> p k) \<and> (d\<beta> q k))" 
-  "d\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
-  "d\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
-  "d\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
-  "d\<beta> p = (\<lambda> k. True)"
+recdef a_\<beta> "measure size"
+  "a_\<beta> (And p q) = (\<lambda> k. And (a_\<beta> p k) (a_\<beta> q k))" 
+  "a_\<beta> (Or p q) = (\<lambda> k. Or (a_\<beta> p k) (a_\<beta> q k))" 
+  "a_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. Eq (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. NEq (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. Lt (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. Le (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. Gt (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. Ge (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. Dvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. NDvd ((k div c)*i) (CN 0 1 (Mul (k div c) e)))"
+  "a_\<beta> p = (\<lambda> k. p)"
+
+recdef d_\<beta> "measure size"
+  "d_\<beta> (And p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))" 
+  "d_\<beta> (Or p q) = (\<lambda> k. (d_\<beta> p k) \<and> (d_\<beta> q k))" 
+  "d_\<beta> (Eq  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d_\<beta> (NEq (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d_\<beta> (Lt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d_\<beta> (Le  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d_\<beta> (Gt  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d_\<beta> (Ge  (CN 0 c e)) = (\<lambda> k. c dvd k)"
+  "d_\<beta> (Dvd i (CN 0 c e)) =(\<lambda> k. c dvd k)"
+  "d_\<beta> (NDvd i (CN 0 c e))=(\<lambda> k. c dvd k)"
+  "d_\<beta> p = (\<lambda> k. True)"
 
 recdef \<zeta> "measure size"
   "\<zeta> (And p q) = lcm (\<zeta> p) (\<zeta> q)" 
@@ -2320,7 +2320,7 @@
   "mirror (NDvd i (CN 0 c e)) = NDvd i (CN 0 c (Neg e))"
   "mirror p = p"
 
-lemma mirror\<alpha>\<beta>:
+lemma mirror_\<alpha>_\<beta>:
   assumes lp: "iszlfm p (a#bs)"
   shows "(Inum (real (i::int)#bs)) ` set (\<alpha> p) = (Inum (real i#bs)) ` set (\<beta> (mirror p))"
 using lp
@@ -2351,8 +2351,8 @@
 lemma mirror_l: "iszlfm p (a#bs) \<Longrightarrow> iszlfm (mirror p) (a#bs)"
 by (induct p rule: mirror.induct, auto simp add: isint_neg)
 
-lemma mirror_d\<beta>: "iszlfm p (a#bs) \<and> d\<beta> p 1 
-  \<Longrightarrow> iszlfm (mirror p) (a#bs) \<and> d\<beta> (mirror p) 1"
+lemma mirror_d_\<beta>: "iszlfm p (a#bs) \<and> d_\<beta> p 1 
+  \<Longrightarrow> iszlfm (mirror p) (a#bs) \<and> d_\<beta> (mirror p) 1"
 by (induct p rule: mirror.induct, auto simp add: isint_neg)
 
 lemma mirror_\<delta>: "iszlfm p (a#bs) \<Longrightarrow> \<delta> (mirror p) = \<delta> p"
@@ -2376,11 +2376,11 @@
   shows "\<forall> b\<in> set (\<beta> p). numbound0 b"
   using lp by (induct p rule: \<beta>.induct,auto)
 
-lemma d\<beta>_mono: 
+lemma d_\<beta>_mono: 
   assumes linp: "iszlfm p (a #bs)"
-  and dr: "d\<beta> p l"
+  and dr: "d_\<beta> p l"
   and d: "l dvd l'"
-  shows "d\<beta> p l'"
+  shows "d_\<beta> p l'"
 using dr linp dvd_trans[of _ "l" "l'", simplified d]
 by (induct p rule: iszlfm.induct) simp_all
 
@@ -2391,26 +2391,26 @@
 
 lemma \<zeta>: 
   assumes linp: "iszlfm p (a #bs)"
-  shows "\<zeta> p > 0 \<and> d\<beta> p (\<zeta> p)"
+  shows "\<zeta> p > 0 \<and> d_\<beta> p (\<zeta> p)"
 using linp
 proof(induct p rule: iszlfm.induct)
   case (1 p q)
   then  have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   from 1 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
-  from 1 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
-    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
+  from 1 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
+    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
     dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
 next
   case (2 p q)
   then have dl1: "\<zeta> p dvd lcm (\<zeta> p) (\<zeta> q)" by simp
   from 2 have dl2: "\<zeta> q dvd lcm (\<zeta> p) (\<zeta> q)" by simp
-  from 2 d\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
-    d\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
+  from 2 d_\<beta>_mono[where p = "p" and l="\<zeta> p" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
+    d_\<beta>_mono[where p = "q" and l="\<zeta> q" and l'="lcm (\<zeta> p) (\<zeta> q)"] 
     dl1 dl2 show ?case by (auto simp add: lcm_pos_int)
 qed (auto simp add: lcm_pos_int)
 
-lemma a\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d\<beta> p l" and lp: "l > 0"
-  shows "iszlfm (a\<beta> p l) (a #bs) \<and> d\<beta> (a\<beta> p l) 1 \<and> (Ifm (real (l * x) #bs) (a\<beta> p l) = Ifm ((real x)#bs) p)"
+lemma a_\<beta>: assumes linp: "iszlfm p (a #bs)" and d: "d_\<beta> p l" and lp: "l > 0"
+  shows "iszlfm (a_\<beta> p l) (a #bs) \<and> d_\<beta> (a_\<beta> p l) 1 \<and> (Ifm (real (l * x) #bs) (a_\<beta> p l) = Ifm ((real x)#bs) p)"
 using linp d
 proof (induct p rule: iszlfm.induct)
   case (5 c e) hence cp: "c>0" and be: "numbound0 e" and ei:"isint e (a#bs)" and d': "c dvd l" by simp+
@@ -2556,20 +2556,20 @@
   finally show ?case using numbound0_I[OF be,where b="real (l * x)" and b'="real x" and bs="bs"] rdvd_def  be  isint_Mul[OF ei]  mult_strict_mono[OF ldcp jp ldcp ] by simp
 qed (simp_all add: numbound0_I[where bs="bs" and b="real (l * x)" and b'="real x"] isint_Mul del: real_of_int_mult)
 
-lemma a\<beta>_ex: assumes linp: "iszlfm p (a#bs)" and d: "d\<beta> p l" and lp: "l>0"
-  shows "(\<exists> x. l dvd x \<and> Ifm (real x #bs) (a\<beta> p l)) = (\<exists> (x::int). Ifm (real x#bs) p)"
+lemma a_\<beta>_ex: assumes linp: "iszlfm p (a#bs)" and d: "d_\<beta> p l" and lp: "l>0"
+  shows "(\<exists> x. l dvd x \<and> Ifm (real x #bs) (a_\<beta> p l)) = (\<exists> (x::int). Ifm (real x#bs) p)"
   (is "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> x. ?P' x)")
 proof-
   have "(\<exists> x. l dvd x \<and> ?P x) = (\<exists> (x::int). ?P (l*x))"
     using unity_coeff_ex[where l="l" and P="?P", simplified] by simp
-  also have "\<dots> = (\<exists> (x::int). ?P' x)" using a\<beta>[OF linp d lp] by simp
+  also have "\<dots> = (\<exists> (x::int). ?P' x)" using a_\<beta>[OF linp d lp] by simp
   finally show ?thesis  . 
 qed
 
 lemma \<beta>:
   assumes lp: "iszlfm p (a#bs)"
-  and u: "d\<beta> p 1"
-  and d: "d\<delta> p d"
+  and u: "d_\<beta> p 1"
+  and d: "d_\<delta> p d"
   and dp: "d > 0"
   and nob: "\<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> (Inum (a#bs)) ` set(\<beta> p). real x = b + real j)"
   and p: "Ifm (real x#bs) p" (is "?P x")
@@ -2705,8 +2705,8 @@
 
 lemma \<beta>':   
   assumes lp: "iszlfm p (a #bs)"
-  and u: "d\<beta> p 1"
-  and d: "d\<delta> p d"
+  and u: "d_\<beta> p 1"
+  and d: "d_\<delta> p d"
   and dp: "d > 0"
   shows "\<forall> x. \<not>(\<exists>(j::int) \<in> {1 .. d}. \<exists> b\<in> set(\<beta> p). Ifm ((Inum (a#bs) b + real j) #bs) p) \<longrightarrow> Ifm (real x#bs) p \<longrightarrow> Ifm (real (x - d)#bs) p" (is "\<forall> x. ?b \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
 proof(clarify)
@@ -2746,8 +2746,8 @@
 
 theorem cp_thm:
   assumes lp: "iszlfm p (a #bs)"
-  and u: "d\<beta> p 1"
-  and d: "d\<delta> p d"
+  and u: "d_\<beta> p 1"
+  and d: "d_\<delta> p d"
   and dp: "d > 0"
   shows "(\<exists> (x::int). Ifm (real x #bs) p) = (\<exists> j\<in> {1.. d}. Ifm (real j #bs) (minusinf p) \<or> (\<exists> b \<in> set (\<beta> p). Ifm ((Inum (a#bs) b + real j) #bs) p))"
   (is "(\<exists> (x::int). ?P (real x)) = (\<exists> j\<in> ?D. ?M j \<or> (\<exists> b\<in> ?B. ?P (?I b + real j)))")
@@ -2775,9 +2775,9 @@
 
 consts 
   \<rho> :: "fm \<Rightarrow> (num \<times> int) list" (* Compute the Reddy and Loveland Bset*)
-  \<sigma>\<rho>:: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm" (* Performs the modified substitution of Reddy and Loveland*)
-  \<alpha>\<rho> :: "fm \<Rightarrow> (num\<times>int) list"
-  a\<rho> :: "fm \<Rightarrow> int \<Rightarrow> fm"
+  \<sigma>_\<rho>:: "fm \<Rightarrow> num \<times> int \<Rightarrow> fm" (* Performs the modified substitution of Reddy and Loveland*)
+  \<alpha>_\<rho> :: "fm \<Rightarrow> (num\<times>int) list"
+  a_\<rho> :: "fm \<Rightarrow> int \<Rightarrow> fm"
 recdef \<rho> "measure size"
   "\<rho> (And p q) = (\<rho> p @ \<rho> q)" 
   "\<rho> (Or p q) = (\<rho> p @ \<rho> q)" 
@@ -2789,52 +2789,52 @@
   "\<rho> (Ge  (CN 0 c e)) = [(Sub (C (-1)) e, c)]"
   "\<rho> p = []"
 
-recdef \<sigma>\<rho> "measure size"
-  "\<sigma>\<rho> (And p q) = (\<lambda> (t,k). And (\<sigma>\<rho> p (t,k)) (\<sigma>\<rho> q (t,k)))" 
-  "\<sigma>\<rho> (Or p q) = (\<lambda> (t,k). Or (\<sigma>\<rho> p (t,k)) (\<sigma>\<rho> q (t,k)))" 
-  "\<sigma>\<rho> (Eq  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Eq (Add (Mul (c div k) t) e)) 
+recdef \<sigma>_\<rho> "measure size"
+  "\<sigma>_\<rho> (And p q) = (\<lambda> (t,k). And (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))" 
+  "\<sigma>_\<rho> (Or p q) = (\<lambda> (t,k). Or (\<sigma>_\<rho> p (t,k)) (\<sigma>_\<rho> q (t,k)))" 
+  "\<sigma>_\<rho> (Eq  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Eq (Add (Mul (c div k) t) e)) 
                                             else (Eq (Add (Mul c t) (Mul k e))))"
-  "\<sigma>\<rho> (NEq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (NEq (Add (Mul (c div k) t) e)) 
+  "\<sigma>_\<rho> (NEq (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (NEq (Add (Mul (c div k) t) e)) 
                                             else (NEq (Add (Mul c t) (Mul k e))))"
-  "\<sigma>\<rho> (Lt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Lt (Add (Mul (c div k) t) e)) 
+  "\<sigma>_\<rho> (Lt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Lt (Add (Mul (c div k) t) e)) 
                                             else (Lt (Add (Mul c t) (Mul k e))))"
-  "\<sigma>\<rho> (Le  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Le (Add (Mul (c div k) t) e)) 
+  "\<sigma>_\<rho> (Le  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Le (Add (Mul (c div k) t) e)) 
                                             else (Le (Add (Mul c t) (Mul k e))))"
-  "\<sigma>\<rho> (Gt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Gt (Add (Mul (c div k) t) e)) 
+  "\<sigma>_\<rho> (Gt  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Gt (Add (Mul (c div k) t) e)) 
                                             else (Gt (Add (Mul c t) (Mul k e))))"
-  "\<sigma>\<rho> (Ge  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Ge (Add (Mul (c div k) t) e)) 
+  "\<sigma>_\<rho> (Ge  (CN 0 c e)) = (\<lambda> (t,k). if k dvd c then (Ge (Add (Mul (c div k) t) e)) 
                                             else (Ge (Add (Mul c t) (Mul k e))))"
-  "\<sigma>\<rho> (Dvd i (CN 0 c e)) =(\<lambda> (t,k). if k dvd c then (Dvd i (Add (Mul (c div k) t) e)) 
+  "\<sigma>_\<rho> (Dvd i (CN 0 c e)) =(\<lambda> (t,k). if k dvd c then (Dvd i (Add (Mul (c div k) t) e)) 
                                             else (Dvd (i*k) (Add (Mul c t) (Mul k e))))"
-  "\<sigma>\<rho> (NDvd i (CN 0 c e))=(\<lambda> (t,k). if k dvd c then (NDvd i (Add (Mul (c div k) t) e)) 
+  "\<sigma>_\<rho> (NDvd i (CN 0 c e))=(\<lambda> (t,k). if k dvd c then (NDvd i (Add (Mul (c div k) t) e)) 
                                             else (NDvd (i*k) (Add (Mul c t) (Mul k e))))"
-  "\<sigma>\<rho> p = (\<lambda> (t,k). p)"
-
-recdef \<alpha>\<rho> "measure size"
-  "\<alpha>\<rho> (And p q) = (\<alpha>\<rho> p @ \<alpha>\<rho> q)" 
-  "\<alpha>\<rho> (Or p q) = (\<alpha>\<rho> p @ \<alpha>\<rho> q)" 
-  "\<alpha>\<rho> (Eq  (CN 0 c e)) = [(Add (C -1) e,c)]"
-  "\<alpha>\<rho> (NEq (CN 0 c e)) = [(e,c)]"
-  "\<alpha>\<rho> (Lt  (CN 0 c e)) = [(e,c)]"
-  "\<alpha>\<rho> (Le  (CN 0 c e)) = [(Add (C -1) e,c)]"
-  "\<alpha>\<rho> p = []"
+  "\<sigma>_\<rho> p = (\<lambda> (t,k). p)"
+
+recdef \<alpha>_\<rho> "measure size"
+  "\<alpha>_\<rho> (And p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)" 
+  "\<alpha>_\<rho> (Or p q) = (\<alpha>_\<rho> p @ \<alpha>_\<rho> q)" 
+  "\<alpha>_\<rho> (Eq  (CN 0 c e)) = [(Add (C -1) e,c)]"
+  "\<alpha>_\<rho> (NEq (CN 0 c e)) = [(e,c)]"
+  "\<alpha>_\<rho> (Lt  (CN 0 c e)) = [(e,c)]"
+  "\<alpha>_\<rho> (Le  (CN 0 c e)) = [(Add (C -1) e,c)]"
+  "\<alpha>_\<rho> p = []"
 
     (* Simulates normal substituion by modifying the formula see correctness theorem *)
 
 definition \<sigma> :: "fm \<Rightarrow> int \<Rightarrow> num \<Rightarrow> fm" where
-  "\<sigma> p k t \<equiv> And (Dvd k t) (\<sigma>\<rho> p (t,k))"
-
-lemma \<sigma>\<rho>:
+  "\<sigma> p k t \<equiv> And (Dvd k t) (\<sigma>_\<rho> p (t,k))"
+
+lemma \<sigma>_\<rho>:
   assumes linp: "iszlfm p (real (x::int)#bs)"
   and kpos: "real k > 0"
   and tnb: "numbound0 t"
   and tint: "isint t (real x#bs)"
   and kdt: "k dvd floor (Inum (b'#bs) t)"
-  shows "Ifm (real x#bs) (\<sigma>\<rho> p (t,k)) = 
+  shows "Ifm (real x#bs) (\<sigma>_\<rho> p (t,k)) = 
   (Ifm ((real ((floor (Inum (b'#bs) t)) div k))#bs) p)" 
   (is "?I (real x) (?s p) = (?I (real ((floor (?N b' t)) div k)) p)" is "_ = (?I ?tk p)")
 using linp kpos tnb
-proof(induct p rule: \<sigma>\<rho>.induct)
+proof(induct p rule: \<sigma>_\<rho>.induct)
   case (3 c e) 
   from 3 have cp: "c > 0" and nb: "numbound0 e" by auto
   { assume kdc: "k dvd c" 
@@ -3033,8 +3033,8 @@
   numbound0_I[where bs="bs" and b="real ((floor (?N b' t)) div k)" and b'="real x"])
 
 
-lemma \<sigma>\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t"
-  shows "bound0 (\<sigma>\<rho> p (t,k))"
+lemma \<sigma>_\<rho>_nb: assumes lp:"iszlfm p (a#bs)" and nb: "numbound0 t"
+  shows "bound0 (\<sigma>_\<rho> p (t,k))"
   using lp
   by (induct p rule: iszlfm.induct, auto simp add: nb)
 
@@ -3043,15 +3043,15 @@
   shows "\<forall> (b,k) \<in> set (\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)"
 using lp by (induct p rule: \<rho>.induct, auto simp add: isint_sub isint_neg)
 
-lemma \<alpha>\<rho>_l:
+lemma \<alpha>_\<rho>_l:
   assumes lp: "iszlfm p (real (i::int)#bs)"
-  shows "\<forall> (b,k) \<in> set (\<alpha>\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)"
+  shows "\<forall> (b,k) \<in> set (\<alpha>_\<rho> p). k >0 \<and> numbound0 b \<and> isint b (real i#bs)"
 using lp isint_add [OF isint_c[where j="- 1"],where bs="real i#bs"]
- by (induct p rule: \<alpha>\<rho>.induct, auto)
+ by (induct p rule: \<alpha>_\<rho>.induct, auto)
 
 lemma \<rho>: assumes lp: "iszlfm p (real (i::int) #bs)"
   and pi: "Ifm (real i#bs) p"
-  and d: "d\<delta> p d"
+  and d: "d_\<delta> p d"
   and dp: "d > 0"
   and nob: "\<forall>(e,c) \<in> set (\<rho> p). \<forall> j\<in> {1 .. c*d}. real (c*i) \<noteq> Inum (real i#bs) e + real j"
   (is "\<forall>(e,c) \<in> set (\<rho> p). \<forall> j\<in> {1 .. c*d}. _ \<noteq> ?N i e + _")
@@ -3187,10 +3187,10 @@
 
 lemma \<sigma>_nb: assumes lp: "iszlfm p (a#bs)" and nb: "numbound0 t"
   shows "bound0 (\<sigma> p k t)"
-  using \<sigma>\<rho>_nb[OF lp nb] nb by (simp add: \<sigma>_def)
+  using \<sigma>_\<rho>_nb[OF lp nb] nb by (simp add: \<sigma>_def)
   
 lemma \<rho>':   assumes lp: "iszlfm p (a #bs)"
-  and d: "d\<delta> p d"
+  and d: "d_\<delta> p d"
   and dp: "d > 0"
   shows "\<forall> x. \<not>(\<exists> (e,c) \<in> set(\<rho> p). \<exists>(j::int) \<in> {1 .. c*d}. Ifm (a #bs) (\<sigma> p c (Add e (C j)))) \<longrightarrow> Ifm (real x#bs) p \<longrightarrow> Ifm (real (x - d)#bs) p" (is "\<forall> x. ?b x \<longrightarrow> ?P x \<longrightarrow> ?P (x - d)")
 proof(clarify)
@@ -3219,8 +3219,8 @@
     from nb have nb': "numbound0 (Add e (C j))" by simp
     have ji: "isint (C j) (real x#bs)" by (simp add: isint_def)
     from isint_add[OF ei ji] have ei':"isint (Add e (C j)) (real x#bs)" .
-    from th \<sigma>\<rho>[where b'="real x", OF lp' cp' nb' ei' cdej',symmetric]
-    have "Ifm (real x#bs) (\<sigma>\<rho> p (Add e (C j), c))" by simp
+    from th \<sigma>_\<rho>[where b'="real x", OF lp' cp' nb' ei' cdej',symmetric]
+    have "Ifm (real x#bs) (\<sigma>_\<rho> p (Add e (C j), c))" by simp
     with rcdej have th: "Ifm (real x#bs) (\<sigma> p c (Add e (C j)))" by (simp add: \<sigma>_def)
     from th bound0_I[OF \<sigma>_nb[OF lp nb', where k="c"],where bs="bs" and b="real x" and b'="a"]
     have "Ifm (a#bs) (\<sigma> p c (Add e (C j)))" by blast
@@ -3237,7 +3237,7 @@
     is "?lhs = (?MD \<or> ?RD)"  is "?lhs = ?rhs")
 proof-
   let ?d= "\<delta> p"
-  from \<delta>[OF lp] have d:"d\<delta> p ?d" and dp: "?d > 0" by auto
+  from \<delta>[OF lp] have d:"d_\<delta> p ?d" and dp: "?d > 0" by auto
   { assume H:"?MD" hence th:"\<exists> (x::int). ?MP x" by blast
     from H minusinf_ex[OF lp th] have ?thesis  by blast}
   moreover
@@ -3251,12 +3251,12 @@
     from spx bound0_I[OF \<sigma>_nb[OF lp nb', where k="c"], where bs="bs" and b="a" and b'="real i"]
     have spx': "Ifm (real i # bs) (\<sigma> p c (Add e (C j)))" by blast
     from spx' have rcdej:"real c rdvd (Inum (real i#bs) (Add e (C j)))" 
-      and sr:"Ifm (real i#bs) (\<sigma>\<rho> p (Add e (C j),c))" by (simp add: \<sigma>_def)+
+      and sr:"Ifm (real i#bs) (\<sigma>_\<rho> p (Add e (C j),c))" by (simp add: \<sigma>_def)+
     from rcdej eji[simplified isint_iff] 
     have "real c rdvd real (floor (Inum (real i#bs) (Add e (C j))))" by simp
     hence cdej:"c dvd floor (Inum (real i#bs) (Add e (C j)))" by (simp only: int_rdvd_iff)
     from cp have cp': "real c > 0" by simp
-    from \<sigma>\<rho>[OF lp cp' nb' eji cdej] spx' have "?P (\<lfloor>Inum (real i # bs) (Add e (C j))\<rfloor> div c)"
+    from \<sigma>_\<rho>[OF lp cp' nb' eji cdej] spx' have "?P (\<lfloor>Inum (real i # bs) (Add e (C j))\<rfloor> div c)"
       by (simp add: \<sigma>_def)
     hence ?lhs by blast
     with exR jD spx have ?thesis by blast}
@@ -3272,8 +3272,8 @@
   ultimately show ?thesis by blast
 qed
 
-lemma mirror_\<alpha>\<rho>:   assumes lp: "iszlfm p (a#bs)"
-  shows "(\<lambda> (t,k). (Inum (a#bs) t, k)) ` set (\<alpha>\<rho> p) = (\<lambda> (t,k). (Inum (a#bs) t,k)) ` set (\<rho> (mirror p))"
+lemma mirror_\<alpha>_\<rho>:   assumes lp: "iszlfm p (a#bs)"
+  shows "(\<lambda> (t,k). (Inum (a#bs) t, k)) ` set (\<alpha>_\<rho> p) = (\<lambda> (t,k). (Inum (a#bs) t,k)) ` set (\<rho> (mirror p))"
 using lp
 by (induct p rule: mirror.induct, simp_all add: split_def image_Un )
   
@@ -4714,7 +4714,7 @@
 qed
 
 
-lemma fr_eq\<upsilon>: 
+lemma fr_eq_\<upsilon>: 
   assumes lp: "isrlfm p"
   shows "(\<exists> x. Ifm (x#bs) p) = ((Ifm (x#bs) (minusinf p)) \<or> (Ifm (x#bs) (plusinf p)) \<or> (\<exists> (t,k) \<in> set (\<Upsilon> p). \<exists> (s,l) \<in> set (\<Upsilon> p). Ifm (x#bs) (\<upsilon> p (Add(Mul l t) (Mul k s) , 2*k*l))))"
   (is "(\<exists> x. ?I x p) = (?M \<or> ?P \<or> ?F)" is "?E = ?D")
@@ -4856,7 +4856,7 @@
     hence lqx: "?I x ?rq " using simpfm[where p="?rq" and bs="x#bs"] by auto
     from qf have qfq:"isrlfm ?rq"  
       by (auto simp add: rsplit_def lt_def ge_def rlfm_I[OF qf xp x1])
-    with lqx fr_eq\<upsilon>[OF qfq] show "?M \<or> ?P \<or> ?F" by blast
+    with lqx fr_eq_\<upsilon>[OF qfq] show "?M \<or> ?P \<or> ?F" by blast
   next
     assume D: "?D"
     let ?U = "set (\<Upsilon> ?rq )"
@@ -5066,27 +5066,27 @@
 
 lemma cp_thm': 
   assumes lp: "iszlfm p (real (i::int)#bs)"
-  and up: "d\<beta> p 1" and dd: "d\<delta> p d" and dp: "d > 0"
+  and up: "d_\<beta> p 1" and dd: "d_\<delta> p d" and dp: "d > 0"
   shows "(\<exists> (x::int). Ifm (real x#bs) p) = ((\<exists> j\<in> {1 .. d}. Ifm (real j#bs) (minusinf p)) \<or> (\<exists> j\<in> {1.. d}. \<exists> b\<in> (Inum (real i#bs)) ` set (\<beta> p). Ifm ((b+real j)#bs) p))"
   using cp_thm[OF lp up dd dp] by auto
 
 definition unit :: "fm \<Rightarrow> fm \<times> num list \<times> int" where
-  "unit p \<equiv> (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a\<beta> p' l); d = \<delta> q;
+  "unit p \<equiv> (let p' = zlfm p ; l = \<zeta> p' ; q = And (Dvd l (CN 0 1 (C 0))) (a_\<beta> p' l); d = \<delta> q;
              B = remdups (map simpnum (\<beta> q)) ; a = remdups (map simpnum (\<alpha> q))
              in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"
 
 lemma unit: assumes qf: "qfree p"
-  shows "\<And> q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and> (Inum (real i#bs)) ` set B = (Inum (real i#bs)) ` set (\<beta> q) \<and> d\<beta> q 1 \<and> d\<delta> q d \<and> d >0 \<and> iszlfm q (real (i::int)#bs) \<and> (\<forall> b\<in> set B. numbound0 b)"
+  shows "\<And> q B d. unit p = (q,B,d) \<Longrightarrow> ((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and> (Inum (real i#bs)) ` set B = (Inum (real i#bs)) ` set (\<beta> q) \<and> d_\<beta> q 1 \<and> d_\<delta> q d \<and> d >0 \<and> iszlfm q (real (i::int)#bs) \<and> (\<forall> b\<in> set B. numbound0 b)"
 proof-
   fix q B d 
   assume qBd: "unit p = (q,B,d)"
   let ?thes = "((\<exists> (x::int). Ifm (real x#bs) p) = (\<exists> (x::int). Ifm (real x#bs) q)) \<and>
     Inum (real i#bs) ` set B = Inum (real i#bs) ` set (\<beta> q) \<and>
-    d\<beta> q 1 \<and> d\<delta> q d \<and> 0 < d \<and> iszlfm q (real i # bs) \<and> (\<forall> b\<in> set B. numbound0 b)"
+    d_\<beta> q 1 \<and> d_\<delta> q d \<and> 0 < d \<and> iszlfm q (real i # bs) \<and> (\<forall> b\<in> set B. numbound0 b)"
   let ?I = "\<lambda> (x::int) p. Ifm (real x#bs) p"
   let ?p' = "zlfm p"
   let ?l = "\<zeta> ?p'"
-  let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a\<beta> ?p' ?l)"
+  let ?q = "And (Dvd ?l (CN 0 1 (C 0))) (a_\<beta> ?p' ?l)"
   let ?d = "\<delta> ?q"
   let ?B = "set (\<beta> ?q)"
   let ?B'= "remdups (map simpnum (\<beta> ?q))"
@@ -5097,12 +5097,12 @@
   from iszlfm_gen[OF conjunct2[OF zlfm_I[OF qf, where bs="bs" and i="i"]]]
   have lp': "\<forall> (i::int). iszlfm ?p' (real i#bs)" by simp 
   hence lp'': "iszlfm ?p' (real (i::int)#bs)" by simp
-  from lp' \<zeta>[where p="?p'" and bs="bs"] have lp: "?l >0" and dl: "d\<beta> ?p' ?l" by auto
-  from a\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp'' dl lp] pp'
+  from lp' \<zeta>[where p="?p'" and bs="bs"] have lp: "?l >0" and dl: "d_\<beta> ?p' ?l" by auto
+  from a_\<beta>_ex[where p="?p'" and l="?l" and bs="bs", OF lp'' dl lp] pp'
   have pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by (simp add: int_rdvd_iff) 
-  from lp'' lp a\<beta>[OF lp'' dl lp] have lq:"iszlfm ?q (real i#bs)" and uq: "d\<beta> ?q 1" 
+  from lp'' lp a_\<beta>[OF lp'' dl lp] have lq:"iszlfm ?q (real i#bs)" and uq: "d_\<beta> ?q 1" 
     by (auto simp add: isint_def)
-  from \<delta>[OF lq] have dp:"?d >0" and dd: "d\<delta> ?q ?d" by blast+
+  from \<delta>[OF lq] have dp:"?d >0" and dd: "d_\<delta> ?q ?d" by blast+
   let ?N = "\<lambda> t. Inum (real (i::int)#bs) t"
   have "?N ` set ?B' = ((?N o simpnum) ` ?B)" by (simp add:image_compose) 
   also have "\<dots> = ?N ` ?B" using simpnum_ci[where bs="real i #bs"] by auto
@@ -5124,13 +5124,13 @@
   {assume "\<not> (length ?B' \<le> length ?A')"
     hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
       using qBd by (auto simp add: Let_def unit_def)
-    with AA' mirror\<alpha>\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)" 
+    with AA' mirror_\<alpha>_\<beta>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<beta> q)" 
       and bn: "\<forall>b\<in> set B. numbound0 b" by simp+
     from mirror_ex[OF lq] pq_ex q 
     have pqm_eq:"(\<exists> (x::int). ?I x p) = (\<exists> (x::int). ?I x q)" by simp
-    from lq uq q mirror_d\<beta> [where p="?q" and bs="bs" and a="real i"]
-    have lq': "iszlfm q (real i#bs)" and uq: "d\<beta> q 1" by auto
-    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d\<delta> q d " by auto
+    from lq uq q mirror_d_\<beta> [where p="?q" and bs="bs" and a="real i"]
+    have lq': "iszlfm q (real i#bs)" and uq: "d_\<beta> q 1" by auto
+    from \<delta>[OF lq'] mirror_\<delta>[OF lq] q d have dq:"d_\<delta> q d " by auto
     from pqm_eq b bn uq lq' dp dq q dp d have ?thes by simp
   }
   ultimately show ?thes by blast
@@ -5168,7 +5168,7 @@
   have qbf:"unit p = (?q,?B,?d)" by simp
   from unit[OF qf qbf] have pq_ex: "(\<exists>(x::int). ?I x p) = (\<exists> (x::int). ?I x ?q)" and 
     B:"?N ` set ?B = ?N ` set (\<beta> ?q)" and 
-    uq:"d\<beta> ?q 1" and dd: "d\<delta> ?q ?d" and dp: "?d > 0" and 
+    uq:"d_\<beta> ?q 1" and dd: "d_\<delta> ?q ?d" and dp: "?d > 0" and 
     lq: "iszlfm ?q (real i#bs)" and 
     Bn: "\<forall> b\<in> set ?B. numbound0 b" by auto
   from zlin_qfree[OF lq] have qfq: "qfree ?q" .
@@ -5231,14 +5231,14 @@
 
     (* Redy and Loveland *)
 
-lemma \<sigma>\<rho>_cong: assumes lp: "iszlfm p (a#bs)" and tt': "Inum (a#bs) t = Inum (a#bs) t'"
-  shows "Ifm (a#bs) (\<sigma>\<rho> p (t,c)) = Ifm (a#bs) (\<sigma>\<rho> p (t',c))"
+lemma \<sigma>_\<rho>_cong: assumes lp: "iszlfm p (a#bs)" and tt': "Inum (a#bs) t = Inum (a#bs) t'"
+  shows "Ifm (a#bs) (\<sigma>_\<rho> p (t,c)) = Ifm (a#bs) (\<sigma>_\<rho> p (t',c))"
   using lp 
   by (induct p rule: iszlfm.induct, auto simp add: tt')
 
 lemma \<sigma>_cong: assumes lp: "iszlfm p (a#bs)" and tt': "Inum (a#bs) t = Inum (a#bs) t'"
   shows "Ifm (a#bs) (\<sigma> p c t) = Ifm (a#bs) (\<sigma> p c t')"
-  by (simp add: \<sigma>_def tt' \<sigma>\<rho>_cong[OF lp tt'])
+  by (simp add: \<sigma>_def tt' \<sigma>_\<rho>_cong[OF lp tt'])
 
 lemma \<rho>_cong: assumes lp: "iszlfm p (a#bs)" 
   and RR: "(\<lambda>(b,k). (Inum (a#bs) b,k)) ` R =  (\<lambda>(b,k). (Inum (a#bs) b,k)) ` set (\<rho> p)"
@@ -5284,7 +5284,7 @@
 definition chooset :: "fm \<Rightarrow> fm \<times> ((num\<times>int) list) \<times> int" where
   "chooset p \<equiv> (let q = zlfm p ; d = \<delta> q;
              B = remdups (map (\<lambda> (t,k). (simpnum t,k)) (\<rho> q)) ; 
-             a = remdups (map (\<lambda> (t,k). (simpnum t,k)) (\<alpha>\<rho> q))
+             a = remdups (map (\<lambda> (t,k). (simpnum t,k)) (\<alpha>_\<rho> q))
              in if length B \<le> length a then (q,B,d) else (mirror q, a,d))"
 
 lemma chooset: assumes qf: "qfree p"
@@ -5299,8 +5299,8 @@
   let ?B = "set (\<rho> ?q)"
   let ?f = "\<lambda> (t,k). (simpnum t,k)"
   let ?B'= "remdups (map ?f (\<rho> ?q))"
-  let ?A = "set (\<alpha>\<rho> ?q)"
-  let ?A'= "remdups (map ?f (\<alpha>\<rho> ?q))"
+  let ?A = "set (\<alpha>_\<rho> ?q)"
+  let ?A'= "remdups (map ?f (\<alpha>_\<rho> ?q))"
   from conjunct1[OF zlfm_I[OF qf, where bs="bs"]] 
   have pp': "\<forall> i. ?I i ?q = ?I i p" by auto
   hence pq_ex:"(\<exists> (x::int). ?I x p) = (\<exists> x. ?I x ?q)" by simp 
@@ -5318,7 +5318,7 @@
   finally have AA': "?N ` set ?A' = ?N ` ?A" .
   from \<rho>_l[OF lq] have B_nb:"\<forall> (e,c)\<in> set ?B'. numbound0 e \<and> c > 0"
     by (simp add: simpnum_numbound0 split_def)
-  from \<alpha>\<rho>_l[OF lq] have A_nb: "\<forall> (e,c)\<in> set ?A'. numbound0 e \<and> c > 0"
+  from \<alpha>_\<rho>_l[OF lq] have A_nb: "\<forall> (e,c)\<in> set ?A'. numbound0 e \<and> c > 0"
     by (simp add: simpnum_numbound0 split_def)
     {assume "length ?B' \<le> length ?A'"
     hence q:"q=?q" and "B = ?B'" and d:"d = ?d"
@@ -5330,7 +5330,7 @@
   {assume "\<not> (length ?B' \<le> length ?A')"
     hence q:"q=mirror ?q" and "B = ?A'" and d:"d = ?d"
       using qBd by (auto simp add: Let_def chooset_def)
-    with AA' mirror_\<alpha>\<rho>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<rho> q)" 
+    with AA' mirror_\<alpha>_\<rho>[OF lq] A_nb have b:"?N ` (set B) = ?N ` set (\<rho> q)" 
       and bn: "\<forall>(e,c)\<in> set B. numbound0 e \<and> c > 0" by auto 
     from mirror_ex[OF lq] pq_ex q 
     have pqm_eq:"(\<exists> (x::int). ?I x p) = (\<exists> (x::int). ?I x q)" by simp
diff -r 227477f17c26 -r 4aa34bd43228 src/HOL/Matrix_LP/LP.thy
--- a/src/HOL/Matrix_LP/LP.thy	Wed Nov 28 15:38:12 2012 +0100
+++ b/src/HOL/Matrix_LP/LP.thy	Wed Nov 28 15:59:18 2012 +0100
@@ -19,12 +19,12 @@
   assumes
   "A * x \<le> (b::'a::lattice_ring)"
   "0 \<le> y"
-  "abs (A - A') \<le> \<delta>A"
+  "abs (A - A') \<le> \<delta>_A"
   "b \<le> b'"
-  "abs (c - c') \<le> \<delta>c"
+  "abs (c - c') \<le> \<delta>_c"
   "abs x \<le> r"
   shows
-  "c * x \<le> y * b' + (y * \<delta>A + abs (y * A' - c') + \<delta>c) * r"
+  "c * x \<le> y * b' + (y * \<delta>_A + abs (y * A' - c') + \<delta>_c) * r"
 proof -
   from assms have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
   from assms have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
@@ -43,20 +43,20 @@
   have 10: "c'-c = -(c-c')" by (simp add: algebra_simps)
   have 11: "abs (c'-c) = abs (c-c')" 
     by (subst 10, subst abs_minus_cancel, simp)
-  have 12: "(abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + \<delta>c) * abs x"
+  have 12: "(abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + \<delta>_c) * abs x"
     by (simp add: 11 assms mult_right_mono)
-  have 13: "(abs y * abs (A-A') + abs (y*A'-c') + \<delta>c) * abs x <= (abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * abs x"
+  have 13: "(abs y * abs (A-A') + abs (y*A'-c') + \<delta>_c) * abs x <= (abs y * \<delta>_A + abs (y*A'-c') + \<delta>_c) * abs x"
     by (simp add: assms mult_right_mono mult_left_mono)  
-  have r: "(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * abs x <=  (abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"
+  have r: "(abs y * \<delta>_A + abs (y*A'-c') + \<delta>_c) * abs x <=  (abs y * \<delta>_A + abs (y*A'-c') + \<delta>_c) * r"
     apply (rule mult_left_mono)
     apply (simp add: assms)
     apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+
-    apply (rule mult_left_mono[of "0" "\<delta>A", simplified])
+    apply (rule mult_left_mono[of "0" "\<delta>_A", simplified])
     apply (simp_all)
     apply (rule order_trans[where y="abs (A-A')"], simp_all add: assms)
     apply (rule order_trans[where y="abs (c-c')"], simp_all add: assms)
     done    
-  from 6 7 8 9 12 13 r have 14:" abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <=(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"     
+  from 6 7 8 9 12 13 r have 14:" abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <=(abs y * \<delta>_A + abs (y*A'-c') + \<delta>_c) * r"     
     by (simp)
   show ?thesis
     apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
diff -r 227477f17c26 -r 4aa34bd43228 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Nov 28 15:38:12 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Nov 28 15:59:18 2012 +0100
@@ -527,16 +527,16 @@
 lemma pi'_range[intro]: "\<And>i::'n. \<pi>' i < CARD('n::finite)"
   using bij_betw_pi' unfolding bij_betw_def by auto
 
-lemma \<pi>\<pi>'[simp]: "\<And>i::'n::finite. \<pi> (\<pi>' i) = i"
+lemma pi_pi'[simp]: "\<And>i::'n::finite. \<pi> (\<pi>' i) = i"
   using bij_betw_pi by (auto intro!: f_inv_into_f simp: \<pi>'_def bij_betw_def)
 
-lemma \<pi>'\<pi>[simp]: "\<And>i. i\<in>{..<CARD('n::finite)} \<Longrightarrow> \<pi>' (\<pi> i::'n) = i"
+lemma pi'_pi[simp]: "\<And>i. i\<in>{..<CARD('n::finite)} \<Longrightarrow> \<pi>' (\<pi> i::'n) = i"
   using bij_betw_pi by (auto intro!: inv_into_f_eq simp: \<pi>'_def bij_betw_def)
 
-lemma \<pi>\<pi>'_alt[simp]: "\<And>i. i<CARD('n::finite) \<Longrightarrow> \<pi>' (\<pi> i::'n) = i"
+lemma pi_pi'_alt[simp]: "\<And>i. i<CARD('n::finite) \<Longrightarrow> \<pi>' (\<pi> i::'n) = i"
   by auto
 
-lemma \<pi>_inj_on: "inj_on (\<pi>::nat\<Rightarrow>'n::finite) {..<CARD('n)}"
+lemma pi_inj_on: "inj_on (\<pi>::nat\<Rightarrow>'n::finite) {..<CARD('n)}"
   using bij_betw_pi[where 'n='n] by (simp add: bij_betw_def)
 
 instantiation vec :: (euclidean_space, finite) euclidean_space
diff -r 227477f17c26 -r 4aa34bd43228 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Wed Nov 28 15:38:12 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Wed Nov 28 15:59:18 2012 +0100
@@ -867,11 +867,11 @@
   guess \<pi> using ex_bij_betw_nat_finite_1[OF finite_lessThan[of "DIM('a)"]] .. note \<pi>=this
   def \<pi>' \<equiv> "inv_into {1..n} \<pi>"
   have \<pi>':"bij_betw \<pi>' {..<DIM('a)} {1..n}" using bij_betw_inv_into[OF \<pi>] unfolding \<pi>'_def n_def by auto
-  hence \<pi>'i:"\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i \<in> {1..n}" unfolding bij_betw_def by auto 
-  have \<pi>i:"\<And>i. i\<in>{1..n} \<Longrightarrow> \<pi> i <DIM('a)" using \<pi> unfolding bij_betw_def n_def by auto 
-  have \<pi>\<pi>'[simp]:"\<And>i. i<DIM('a) \<Longrightarrow> \<pi> (\<pi>' i) = i" unfolding \<pi>'_def
+  hence \<pi>'_i:"\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i \<in> {1..n}" unfolding bij_betw_def by auto 
+  have \<pi>_i:"\<And>i. i\<in>{1..n} \<Longrightarrow> \<pi> i <DIM('a)" using \<pi> unfolding bij_betw_def n_def by auto 
+  have \<pi>_\<pi>'[simp]:"\<And>i. i<DIM('a) \<Longrightarrow> \<pi> (\<pi>' i) = i" unfolding \<pi>'_def
     apply(rule f_inv_into_f) unfolding n_def using \<pi> unfolding bij_betw_def by auto
-  have \<pi>'\<pi>[simp]:"\<And>i. i\<in>{1..n} \<Longrightarrow> \<pi>' (\<pi> i) = i" unfolding \<pi>'_def apply(rule inv_into_f_eq)
+  have \<pi>'_\<pi>[simp]:"\<And>i. i\<in>{1..n} \<Longrightarrow> \<pi>' (\<pi> i) = i" unfolding \<pi>'_def apply(rule inv_into_f_eq)
     using \<pi> unfolding n_def bij_betw_def by auto
   have "{c..d} \<noteq> {}" using assms by auto
   let ?p1 = "\<lambda>l. {(\<chi>\<chi> i. if \<pi>' i < l then c$$i else a$$i)::'a .. (\<chi>\<chi> i. if \<pi>' i < l then d$$i else if \<pi>' i = l then c$$\<pi> l else b$$i)}"
@@ -943,47 +943,47 @@
       assume "l \<le> l'" fix x
       have "x \<notin> interior k \<inter> interior k'" 
       proof(rule,cases "l' = n+1") assume x:"x \<in> interior k \<inter> interior k'"
-        case True hence "\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i < l'" using \<pi>'i using l' by(auto simp add:less_Suc_eq_le)
+        case True hence "\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i < l'" using \<pi>'_i using l' by(auto simp add:less_Suc_eq_le)
         hence *:"\<And> P Q. (\<chi>\<chi> i. if \<pi>' i < l' then P i else Q i) = ((\<chi>\<chi> i. P i)::'a)" apply-apply(subst euclidean_eq) by auto
         hence k':"k' = {c..d}" using l'(1) unfolding * by auto
         have ln:"l < n + 1" 
         proof(rule ccontr) case goal1 hence l2:"l = n+1" using l by auto
-          hence "\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i < l" using \<pi>'i by(auto simp add:less_Suc_eq_le)
+          hence "\<And>i. i<DIM('a) \<Longrightarrow> \<pi>' i < l" using \<pi>'_i by(auto simp add:less_Suc_eq_le)
           hence *:"\<And> P Q. (\<chi>\<chi> i. if \<pi>' i < l then P i else Q i) = ((\<chi>\<chi> i. P i)::'a)" apply-apply(subst euclidean_eq) by auto
-          hence "k = {c..d}" using l(1) \<pi>'i unfolding * by(auto)
+          hence "k = {c..d}" using l(1) \<pi>'_i unfolding * by(auto)
           thus False using `k\<noteq>k'` k' by auto
-        qed have **:"\<pi>' (\<pi> l) = l" using \<pi>'\<pi>[of l] using l ln by auto
+        qed have **:"\<pi>' (\<pi> l) = l" using \<pi>'_\<pi>[of l] using l ln by auto
         have "x $$ \<pi> l < c $$ \<pi> l \<or> d $$ \<pi> l < x $$ \<pi> l" using l(1) apply-
         proof(erule disjE)
           assume as:"k = ?p1 l" note * = conjunct1[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
-          show ?thesis using *[of "\<pi> l"] using ln l(2) using \<pi>i[of l] by(auto simp add:** not_less)
+          show ?thesis using *[of "\<pi> l"] using ln l(2) using \<pi>_i[of l] by(auto simp add:** not_less)
         next assume as:"k = ?p2 l" note * = conjunct1[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
-          show ?thesis using *[of "\<pi> l"] using ln l(2) using \<pi>i[of l] unfolding ** by auto
+          show ?thesis using *[of "\<pi> l"] using ln l(2) using \<pi>_i[of l] unfolding ** by auto
         qed thus False using x unfolding k' unfolding Int_iff interior_closed_interval mem_interval
           by(auto elim!:allE[where x="\<pi> l"])
       next case False hence "l < n + 1" using l'(2) using `l\<le>l'` by auto
         hence ln:"l \<in> {1..n}" "l' \<in> {1..n}" using l l' False by auto
-        note \<pi>l = \<pi>'\<pi>[OF ln(1)] \<pi>'\<pi>[OF ln(2)]
+        note \<pi>_l = \<pi>'_\<pi>[OF ln(1)] \<pi>'_\<pi>[OF ln(2)]
         assume x:"x \<in> interior k \<inter> interior k'"
         show False using l(1) l'(1) apply-
         proof(erule_tac[!] disjE)+
           assume as:"k = ?p1 l" "k' = ?p1 l'"
           note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
           have "l \<noteq> l'" using k'(2)[unfolded as] by auto
-          thus False using *[of "\<pi> l'"] *[of "\<pi> l"] ln using \<pi>i[OF ln(1)] \<pi>i[OF ln(2)] apply(cases "l<l'")
-            by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def)
+          thus False using *[of "\<pi> l'"] *[of "\<pi> l"] ln using \<pi>_i[OF ln(1)] \<pi>_i[OF ln(2)] apply(cases "l<l'")
+            by(auto simp add:euclidean_lambda_beta' \<pi>_l \<pi>_i n_def)
         next assume as:"k = ?p2 l" "k' = ?p2 l'"
           note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
           have "l \<noteq> l'" apply(rule) using k'(2)[unfolded as] by auto
-          thus False using *[of "\<pi> l"] *[of "\<pi> l'"]  `l \<le> l'` ln by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def)
+          thus False using *[of "\<pi> l"] *[of "\<pi> l'"]  `l \<le> l'` ln by(auto simp add:euclidean_lambda_beta' \<pi>_l \<pi>_i n_def)
         next assume as:"k = ?p1 l" "k' = ?p2 l'"
           note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
           show False using abcd[of "\<pi> l'"] using *[of "\<pi> l"] *[of "\<pi> l'"]  `l \<le> l'` ln apply(cases "l=l'")
-            by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def)
+            by(auto simp add:euclidean_lambda_beta' \<pi>_l \<pi>_i n_def)
         next assume as:"k = ?p2 l" "k' = ?p1 l'"
           note * = conjunctD2[OF x[unfolded as Int_iff interior_closed_interval mem_interval],rule_format]
           show False using *[of "\<pi> l"] *[of "\<pi> l'"] ln `l \<le> l'` apply(cases "l=l'") using abcd[of "\<pi> l'"] 
-            by(auto simp add:euclidean_lambda_beta' \<pi>l \<pi>i n_def)
+            by(auto simp add:euclidean_lambda_beta' \<pi>_l \<pi>_i n_def)
         qed qed } 
     from this[OF k l k' l'] this[OF k'(1) l' k _ l] have "\<And>x. x \<notin> interior k \<inter> interior k'"
       apply - apply(cases "l' \<le> l") using k'(2) by auto            
diff -r 227477f17c26 -r 4aa34bd43228 src/HOL/Nominal/Examples/Class3.thy
--- a/src/HOL/Nominal/Examples/Class3.thy	Wed Nov 28 15:38:12 2012 +0100
+++ b/src/HOL/Nominal/Examples/Class3.thy	Wed Nov 28 15:59:18 2012 +0100
@@ -3091,22 +3091,22 @@
  findn :: "(name\<times>coname\<times>trm) list\<Rightarrow>name\<Rightarrow>(coname\<times>trm) option"
 where
   "findn [] x = None"
-| "findn ((y,c,P)#\<theta>n) x = (if y=x then Some (c,P) else findn \<theta>n x)"
+| "findn ((y,c,P)#\<theta>_n) x = (if y=x then Some (c,P) else findn \<theta>_n x)"
 
 lemma findn_eqvt[eqvt]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
-  shows "(pi1\<bullet>findn \<theta>n x) = findn (pi1\<bullet>\<theta>n) (pi1\<bullet>x)" 
-  and   "(pi2\<bullet>findn \<theta>n x) = findn (pi2\<bullet>\<theta>n) (pi2\<bullet>x)"
-apply(induct \<theta>n)
+  shows "(pi1\<bullet>findn \<theta>_n x) = findn (pi1\<bullet>\<theta>_n) (pi1\<bullet>x)" 
+  and   "(pi2\<bullet>findn \<theta>_n x) = findn (pi2\<bullet>\<theta>_n) (pi2\<bullet>x)"
+apply(induct \<theta>_n)
 apply(auto simp add: perm_bij) 
 done
 
 lemma findn_fresh:
-  assumes a: "x\<sharp>\<theta>n"
-  shows "findn \<theta>n x = None"
+  assumes a: "x\<sharp>\<theta>_n"
+  shows "findn \<theta>_n x = None"
 using a
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
 apply(auto simp add: fresh_list_cons fresh_atm fresh_prod)
 done
 
@@ -3114,38 +3114,38 @@
  findc :: "(coname\<times>name\<times>trm) list\<Rightarrow>coname\<Rightarrow>(name\<times>trm) option"
 where
   "findc [] x = None"
-| "findc ((c,y,P)#\<theta>c) a = (if a=c then Some (y,P) else findc \<theta>c a)"
+| "findc ((c,y,P)#\<theta>_c) a = (if a=c then Some (y,P) else findc \<theta>_c a)"
 
 lemma findc_eqvt[eqvt]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
-  shows "(pi1\<bullet>findc \<theta>c a) = findc (pi1\<bullet>\<theta>c) (pi1\<bullet>a)" 
-  and   "(pi2\<bullet>findc \<theta>c a) = findc (pi2\<bullet>\<theta>c) (pi2\<bullet>a)"
-apply(induct \<theta>c)
+  shows "(pi1\<bullet>findc \<theta>_c a) = findc (pi1\<bullet>\<theta>_c) (pi1\<bullet>a)" 
+  and   "(pi2\<bullet>findc \<theta>_c a) = findc (pi2\<bullet>\<theta>_c) (pi2\<bullet>a)"
+apply(induct \<theta>_c)
 apply(auto simp add: perm_bij) 
 done
 
 lemma findc_fresh:
-  assumes a: "a\<sharp>\<theta>c"
-  shows "findc \<theta>c a = None"
+  assumes a: "a\<sharp>\<theta>_c"
+  shows "findc \<theta>_c a = None"
 using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
 apply(auto simp add: fresh_list_cons fresh_atm fresh_prod)
 done
 
 abbreviation 
  nmaps :: "(name\<times>coname\<times>trm) list \<Rightarrow> name \<Rightarrow> (coname\<times>trm) option \<Rightarrow> bool" ("_ nmaps _ to _" [55,55,55] 55) 
 where
- "\<theta>n nmaps x to P \<equiv> (findn \<theta>n x) = P"
+ "\<theta>_n nmaps x to P \<equiv> (findn \<theta>_n x) = P"
 
 abbreviation 
  cmaps :: "(coname\<times>name\<times>trm) list \<Rightarrow> coname \<Rightarrow> (name\<times>trm) option \<Rightarrow> bool" ("_ cmaps _ to _" [55,55,55] 55) 
 where
- "\<theta>c cmaps a to P \<equiv> (findc \<theta>c a) = P"
+ "\<theta>_c cmaps a to P \<equiv> (findc \<theta>_c a) = P"
 
 lemma nmaps_fresh:
-  shows "\<theta>n nmaps x to Some (c,P) \<Longrightarrow> a\<sharp>\<theta>n \<Longrightarrow> a\<sharp>(c,P)"
-apply(induct \<theta>n)
+  shows "\<theta>_n nmaps x to Some (c,P) \<Longrightarrow> a\<sharp>\<theta>_n \<Longrightarrow> a\<sharp>(c,P)"
+apply(induct \<theta>_n)
 apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
 apply(case_tac "aa=x")
 apply(auto)
@@ -3154,8 +3154,8 @@
 done
 
 lemma cmaps_fresh:
-  shows "\<theta>c cmaps a to Some (y,P) \<Longrightarrow> x\<sharp>\<theta>c \<Longrightarrow> x\<sharp>(y,P)"
-apply(induct \<theta>c)
+  shows "\<theta>_c cmaps a to Some (y,P) \<Longrightarrow> x\<sharp>\<theta>_c \<Longrightarrow> x\<sharp>(y,P)"
+apply(induct \<theta>_c)
 apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
 apply(case_tac "a=aa")
 apply(auto)
@@ -3164,14 +3164,14 @@
 done
 
 lemma nmaps_false:
-  shows "\<theta>n nmaps x to Some (c,P) \<Longrightarrow> x\<sharp>\<theta>n \<Longrightarrow> False"
-apply(induct \<theta>n)
+  shows "\<theta>_n nmaps x to Some (c,P) \<Longrightarrow> x\<sharp>\<theta>_n \<Longrightarrow> False"
+apply(induct \<theta>_n)
 apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
 done
 
 lemma cmaps_false:
-  shows "\<theta>c cmaps c to Some (x,P) \<Longrightarrow> c\<sharp>\<theta>c \<Longrightarrow> False"
-apply(induct \<theta>c)
+  shows "\<theta>_c cmaps c to Some (x,P) \<Longrightarrow> c\<sharp>\<theta>_c \<Longrightarrow> False"
+apply(induct \<theta>_c)
 apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
 done
 
@@ -3179,25 +3179,25 @@
  lookupa :: "name\<Rightarrow>coname\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm"
 where
   "lookupa x a [] = Ax x a"
-| "lookupa x a ((c,y,P)#\<theta>c) = (if a=c then Cut <a>.Ax x a (y).P else lookupa x a \<theta>c)"
+| "lookupa x a ((c,y,P)#\<theta>_c) = (if a=c then Cut <a>.Ax x a (y).P else lookupa x a \<theta>_c)"
 
 lemma lookupa_eqvt[eqvt]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
-  shows "(pi1\<bullet>(lookupa x a \<theta>c)) = lookupa (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>c)"
-  and   "(pi2\<bullet>(lookupa x a \<theta>c)) = lookupa (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>c)"
+  shows "(pi1\<bullet>(lookupa x a \<theta>_c)) = lookupa (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>_c)"
+  and   "(pi2\<bullet>(lookupa x a \<theta>_c)) = lookupa (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>_c)"
 apply -
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
 apply(auto simp add: eqvts)
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
 apply(auto simp add: eqvts)
 done
 
 lemma lookupa_fire:
-  assumes a: "\<theta>c cmaps a to Some (y,P)"
-  shows "(lookupa x a \<theta>c) = Cut <a>.Ax x a (y).P"
+  assumes a: "\<theta>_c cmaps a to Some (y,P)"
+  shows "(lookupa x a \<theta>_c) = Cut <a>.Ax x a (y).P"
 using a
-apply(induct \<theta>c arbitrary: x a y P)
+apply(induct \<theta>_c arbitrary: x a y P)
 apply(auto)
 done
 
@@ -3205,35 +3205,35 @@
  lookupb :: "name\<Rightarrow>coname\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>coname\<Rightarrow>trm\<Rightarrow>trm"
 where
   "lookupb x a [] c P = Cut <c>.P (x).Ax x a"
-| "lookupb x a ((d,y,N)#\<theta>c) c P = (if a=d then Cut <c>.P (y).N  else lookupb x a \<theta>c c P)"
+| "lookupb x a ((d,y,N)#\<theta>_c) c P = (if a=d then Cut <c>.P (y).N  else lookupb x a \<theta>_c c P)"
 
 lemma lookupb_eqvt[eqvt]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
-  shows "(pi1\<bullet>(lookupb x a \<theta>c c P)) = lookupb (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>c) (pi1\<bullet>c) (pi1\<bullet>P)"
-  and   "(pi2\<bullet>(lookupb x a \<theta>c c P)) = lookupb (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>c) (pi2\<bullet>c) (pi2\<bullet>P)"
+  shows "(pi1\<bullet>(lookupb x a \<theta>_c c P)) = lookupb (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>_c) (pi1\<bullet>c) (pi1\<bullet>P)"
+  and   "(pi2\<bullet>(lookupb x a \<theta>_c c P)) = lookupb (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>_c) (pi2\<bullet>c) (pi2\<bullet>P)"
 apply -
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
 apply(auto simp add: eqvts)
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
 apply(auto simp add: eqvts)
 done
 
 fun 
   lookup :: "name\<Rightarrow>coname\<Rightarrow>(name\<times>coname\<times>trm) list\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm"
 where
-  "lookup x a [] \<theta>c = lookupa x a \<theta>c"
-| "lookup x a ((y,c,P)#\<theta>n) \<theta>c = (if x=y then (lookupb x a \<theta>c c P) else lookup x a \<theta>n \<theta>c)"
+  "lookup x a [] \<theta>_c = lookupa x a \<theta>_c"
+| "lookup x a ((y,c,P)#\<theta>_n) \<theta>_c = (if x=y then (lookupb x a \<theta>_c c P) else lookup x a \<theta>_n \<theta>_c)"
 
 lemma lookup_eqvt[eqvt]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
-  shows "(pi1\<bullet>(lookup x a \<theta>n \<theta>c)) = lookup (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>n) (pi1\<bullet>\<theta>c)"
-  and   "(pi2\<bullet>(lookup x a \<theta>n \<theta>c)) = lookup (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>n) (pi2\<bullet>\<theta>c)"
+  shows "(pi1\<bullet>(lookup x a \<theta>_n \<theta>_c)) = lookup (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>_n) (pi1\<bullet>\<theta>_c)"
+  and   "(pi2\<bullet>(lookup x a \<theta>_n \<theta>_c)) = lookup (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>_n) (pi2\<bullet>\<theta>_c)"
 apply -
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
 apply(auto simp add: eqvts)
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
 apply(auto simp add: eqvts)
 done
 
@@ -3241,17 +3241,17 @@
   lookupc :: "name\<Rightarrow>coname\<Rightarrow>(name\<times>coname\<times>trm) list\<Rightarrow>trm"
 where
   "lookupc x a [] = Ax x a"
-| "lookupc x a ((y,c,P)#\<theta>n) = (if x=y then P[c\<turnstile>c>a] else lookupc x a \<theta>n)"
+| "lookupc x a ((y,c,P)#\<theta>_n) = (if x=y then P[c\<turnstile>c>a] else lookupc x a \<theta>_n)"
 
 lemma lookupc_eqvt[eqvt]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
-  shows "(pi1\<bullet>(lookupc x a \<theta>n)) = lookupc (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>n)"
-  and   "(pi2\<bullet>(lookupc x a \<theta>n)) = lookupc (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>n)"
+  shows "(pi1\<bullet>(lookupc x a \<theta>_n)) = lookupc (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>_n)"
+  and   "(pi2\<bullet>(lookupc x a \<theta>_n)) = lookupc (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>_n)"
 apply -
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
 apply(auto simp add: eqvts)
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
 apply(auto simp add: eqvts)
 done
 
@@ -3259,47 +3259,47 @@
   lookupd :: "name\<Rightarrow>coname\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm"
 where
   "lookupd x a [] = Ax x a"
-| "lookupd x a ((c,y,P)#\<theta>c) = (if a=c then P[y\<turnstile>n>x] else lookupd x a \<theta>c)"
+| "lookupd x a ((c,y,P)#\<theta>_c) = (if a=c then P[y\<turnstile>n>x] else lookupd x a \<theta>_c)"
 
 lemma lookupd_eqvt[eqvt]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
-  shows "(pi1\<bullet>(lookupd x a \<theta>n)) = lookupd (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>n)"
-  and   "(pi2\<bullet>(lookupd x a \<theta>n)) = lookupd (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>n)"
+  shows "(pi1\<bullet>(lookupd x a \<theta>_n)) = lookupd (pi1\<bullet>x) (pi1\<bullet>a) (pi1\<bullet>\<theta>_n)"
+  and   "(pi2\<bullet>(lookupd x a \<theta>_n)) = lookupd (pi2\<bullet>x) (pi2\<bullet>a) (pi2\<bullet>\<theta>_n)"
 apply -
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
 apply(auto simp add: eqvts)
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
 apply(auto simp add: eqvts)
 done
 
 lemma lookupa_fresh:
-  assumes a: "a\<sharp>\<theta>c"
-  shows "lookupa y a \<theta>c = Ax y a"
+  assumes a: "a\<sharp>\<theta>_c"
+  shows "lookupa y a \<theta>_c = Ax y a"
 using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
 apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
 done
 
 lemma lookupa_csubst:
-  assumes a: "a\<sharp>\<theta>c"
-  shows "Cut <a>.Ax y a (x).P = (lookupa y a \<theta>c){a:=(x).P}"
+  assumes a: "a\<sharp>\<theta>_c"
+  shows "Cut <a>.Ax y a (x).P = (lookupa y a \<theta>_c){a:=(x).P}"
 using a by (simp add: lookupa_fresh)
 
 lemma lookupa_freshness:
   fixes a::"coname"
   and   x::"name"
-  shows "a\<sharp>(\<theta>c,c) \<Longrightarrow> a\<sharp>lookupa y c \<theta>c"
-  and   "x\<sharp>(\<theta>c,y) \<Longrightarrow> x\<sharp>lookupa y c \<theta>c"
-apply(induct \<theta>c)
+  shows "a\<sharp>(\<theta>_c,c) \<Longrightarrow> a\<sharp>lookupa y c \<theta>_c"
+  and   "x\<sharp>(\<theta>_c,y) \<Longrightarrow> x\<sharp>lookupa y c \<theta>_c"
+apply(induct \<theta>_c)
 apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
 done
 
 lemma lookupa_unicity:
-  assumes a: "lookupa x a \<theta>c= Ax y b" "b\<sharp>\<theta>c" "y\<sharp>\<theta>c"
+  assumes a: "lookupa x a \<theta>_c= Ax y b" "b\<sharp>\<theta>_c" "y\<sharp>\<theta>_c"
   shows "x=y \<and> a=b"
 using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
 apply(auto simp add: trm.inject fresh_list_cons fresh_prod fresh_atm)
 apply(case_tac "a=aa")
 apply(auto)
@@ -3308,10 +3308,10 @@
 done
 
 lemma lookupb_csubst:
-  assumes a: "a\<sharp>(\<theta>c,c,N)"
-  shows "Cut <c>.N (x).P = (lookupb y a \<theta>c c N){a:=(x).P}"
+  assumes a: "a\<sharp>(\<theta>_c,c,N)"
+  shows "Cut <c>.N (x).P = (lookupb y a \<theta>_c c N){a:=(x).P}"
 using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
 apply(auto simp add: fresh_list_cons fresh_atm fresh_prod)
 apply(rule sym)
 apply(generate_fresh "name")
@@ -3337,17 +3337,17 @@
 lemma lookupb_freshness:
   fixes a::"coname"
   and   x::"name"
-  shows "a\<sharp>(\<theta>c,c,b,P) \<Longrightarrow> a\<sharp>lookupb y c \<theta>c b P"
-  and   "x\<sharp>(\<theta>c,y,P) \<Longrightarrow> x\<sharp>lookupb y c \<theta>c b P"
-apply(induct \<theta>c)
+  shows "a\<sharp>(\<theta>_c,c,b,P) \<Longrightarrow> a\<sharp>lookupb y c \<theta>_c b P"
+  and   "x\<sharp>(\<theta>_c,y,P) \<Longrightarrow> x\<sharp>lookupb y c \<theta>_c b P"
+apply(induct \<theta>_c)
 apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
 done
 
 lemma lookupb_unicity:
-  assumes a: "lookupb x a \<theta>c c P = Ax y b" "b\<sharp>(\<theta>c,c,P)" "y\<sharp>\<theta>c"
+  assumes a: "lookupb x a \<theta>_c c P = Ax y b" "b\<sharp>(\<theta>_c,c,P)" "y\<sharp>\<theta>_c"
   shows "x=y \<and> a=b"
 using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
 apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
 apply(case_tac "a=aa")
 apply(auto)
@@ -3356,10 +3356,10 @@
 done
 
 lemma lookupb_lookupa:
-  assumes a: "x\<sharp>\<theta>c"
-  shows "lookupb x c \<theta>c a P = (lookupa x c \<theta>c){x:=<a>.P}"
+  assumes a: "x\<sharp>\<theta>_c"
+  shows "lookupb x c \<theta>_c a P = (lookupa x c \<theta>_c){x:=<a>.P}"
 using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
 apply(auto simp add: fresh_list_cons fresh_prod)
 apply(generate_fresh "coname")
 apply(generate_fresh "name")
@@ -3383,10 +3383,10 @@
 done
 
 lemma lookup_csubst:
-  assumes a: "a\<sharp>(\<theta>n,\<theta>c)"
-  shows "lookup y c \<theta>n ((a,x,P)#\<theta>c) = (lookup y c \<theta>n \<theta>c){a:=(x).P}"
+  assumes a: "a\<sharp>(\<theta>_n,\<theta>_c)"
+  shows "lookup y c \<theta>_n ((a,x,P)#\<theta>_c) = (lookup y c \<theta>_n \<theta>_c){a:=(x).P}"
 using a
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
 apply(auto simp add: fresh_prod fresh_list_cons)
 apply(simp add: lookupa_csubst)
 apply(simp add: lookupa_freshness forget fresh_atm fresh_prod)
@@ -3396,18 +3396,18 @@
 done
 
 lemma lookup_fresh:
-  assumes a: "x\<sharp>(\<theta>n,\<theta>c)"
-  shows "lookup x c \<theta>n \<theta>c = lookupa x c \<theta>c"
+  assumes a: "x\<sharp>(\<theta>_n,\<theta>_c)"
+  shows "lookup x c \<theta>_n \<theta>_c = lookupa x c \<theta>_c"
 using a
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
 apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
 done
 
 lemma lookup_unicity:
-  assumes a: "lookup x a \<theta>n \<theta>c= Ax y b" "b\<sharp>(\<theta>c,\<theta>n)" "y\<sharp>(\<theta>c,\<theta>n)"
+  assumes a: "lookup x a \<theta>_n \<theta>_c= Ax y b" "b\<sharp>(\<theta>_c,\<theta>_n)" "y\<sharp>(\<theta>_c,\<theta>_n)"
   shows "x=y \<and> a=b"
 using a
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
 apply(auto simp add: trm.inject fresh_list_cons fresh_prod fresh_atm)
 apply(drule lookupa_unicity)
 apply(simp)+
@@ -3430,9 +3430,9 @@
 lemma lookup_freshness:
   fixes a::"coname"
   and   x::"name"
-  shows "a\<sharp>(c,\<theta>c,\<theta>n) \<Longrightarrow> a\<sharp>lookup y c \<theta>n \<theta>c"
-  and   "x\<sharp>(y,\<theta>c,\<theta>n) \<Longrightarrow> x\<sharp>lookup y c \<theta>n \<theta>c"   
-apply(induct \<theta>n)
+  shows "a\<sharp>(c,\<theta>_c,\<theta>_n) \<Longrightarrow> a\<sharp>lookup y c \<theta>_n \<theta>_c"
+  and   "x\<sharp>(y,\<theta>_c,\<theta>_n) \<Longrightarrow> x\<sharp>lookup y c \<theta>_n \<theta>_c"   
+apply(induct \<theta>_n)
 apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
 apply(simp add: fresh_atm fresh_prod lookupa_freshness)
 apply(simp add: fresh_atm fresh_prod lookupa_freshness)
@@ -3443,9 +3443,9 @@
 lemma lookupc_freshness:
   fixes a::"coname"
   and   x::"name"
-  shows "a\<sharp>(\<theta>c,c) \<Longrightarrow> a\<sharp>lookupc y c \<theta>c"
-  and   "x\<sharp>(\<theta>c,y) \<Longrightarrow> x\<sharp>lookupc y c \<theta>c"
-apply(induct \<theta>c)
+  shows "a\<sharp>(\<theta>_c,c) \<Longrightarrow> a\<sharp>lookupc y c \<theta>_c"
+  and   "x\<sharp>(\<theta>_c,y) \<Longrightarrow> x\<sharp>lookupc y c \<theta>_c"
+apply(induct \<theta>_c)
 apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
 apply(rule rename_fresh)
 apply(simp add: fresh_atm)
@@ -3454,26 +3454,26 @@
 done
 
 lemma lookupc_fresh:
-  assumes a: "y\<sharp>\<theta>n"
-  shows "lookupc y a \<theta>n = Ax y a"
+  assumes a: "y\<sharp>\<theta>_n"
+  shows "lookupc y a \<theta>_n = Ax y a"
 using a
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
 apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
 done
 
 lemma lookupc_nmaps:
-  assumes a: "\<theta>n nmaps x to Some (c,P)"
-  shows "lookupc x a \<theta>n = P[c\<turnstile>c>a]"
+  assumes a: "\<theta>_n nmaps x to Some (c,P)"
+  shows "lookupc x a \<theta>_n = P[c\<turnstile>c>a]"
 using a
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
 apply(auto)
 done 
 
 lemma lookupc_unicity:
-  assumes a: "lookupc y a \<theta>n = Ax x b" "x\<sharp>\<theta>n"
+  assumes a: "lookupc y a \<theta>_n = Ax x b" "x\<sharp>\<theta>_n"
   shows "y=x"
 using a
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
 apply(auto simp add: trm.inject fresh_list_cons fresh_prod)
 apply(case_tac "y=aa")
 apply(auto)
@@ -3484,18 +3484,18 @@
 done
 
 lemma lookupd_fresh:
-  assumes a: "a\<sharp>\<theta>c"
-  shows "lookupd y a \<theta>c = Ax y a"
+  assumes a: "a\<sharp>\<theta>_c"
+  shows "lookupd y a \<theta>_c = Ax y a"
 using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
 apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)
 done 
 
 lemma lookupd_unicity:
-  assumes a: "lookupd y a \<theta>c = Ax y b" "b\<sharp>\<theta>c"
+  assumes a: "lookupd y a \<theta>_c = Ax y b" "b\<sharp>\<theta>_c"
   shows "a=b"
 using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
 apply(auto simp add: trm.inject fresh_list_cons fresh_prod)
 apply(case_tac "a=aa")
 apply(auto)
@@ -3508,9 +3508,9 @@
 lemma lookupd_freshness:
   fixes a::"coname"
   and   x::"name"
-  shows "a\<sharp>(\<theta>c,c) \<Longrightarrow> a\<sharp>lookupd y c \<theta>c"
-  and   "x\<sharp>(\<theta>c,y) \<Longrightarrow> x\<sharp>lookupd y c \<theta>c"
-apply(induct \<theta>c)
+  shows "a\<sharp>(\<theta>_c,c) \<Longrightarrow> a\<sharp>lookupd y c \<theta>_c"
+  and   "x\<sharp>(\<theta>_c,y) \<Longrightarrow> x\<sharp>lookupd y c \<theta>_c"
+apply(induct \<theta>_c)
 apply(auto simp add: fresh_prod fresh_list_cons abs_fresh fresh_atm)
 apply(rule rename_fresh)
 apply(simp add: fresh_atm)
@@ -3519,49 +3519,49 @@
 done
 
 lemma lookupd_cmaps:
-  assumes a: "\<theta>c cmaps a to Some (x,P)"
-  shows "lookupd y a \<theta>c = P[x\<turnstile>n>y]"
+  assumes a: "\<theta>_c cmaps a to Some (x,P)"
+  shows "lookupd y a \<theta>_c = P[x\<turnstile>n>y]"
 using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
 apply(auto)
 done 
 
-nominal_primrec (freshness_context: "\<theta>n::(name\<times>coname\<times>trm)")
+nominal_primrec (freshness_context: "\<theta>_n::(name\<times>coname\<times>trm)")
   stn :: "trm\<Rightarrow>(name\<times>coname\<times>trm) list\<Rightarrow>trm" 
 where
-  "stn (Ax x a) \<theta>n = lookupc x a \<theta>n"
-| "\<lbrakk>a\<sharp>(N,\<theta>n);x\<sharp>(M,\<theta>n)\<rbrakk> \<Longrightarrow> stn (Cut <a>.M (x).N) \<theta>n = (Cut <a>.M (x).N)" 
-| "x\<sharp>\<theta>n \<Longrightarrow> stn (NotR (x).M a) \<theta>n = (NotR (x).M a)"
-| "a\<sharp>\<theta>n \<Longrightarrow>stn (NotL <a>.M x) \<theta>n = (NotL <a>.M x)"
-| "\<lbrakk>a\<sharp>(N,d,b,\<theta>n);b\<sharp>(M,d,a,\<theta>n)\<rbrakk> \<Longrightarrow> stn (AndR <a>.M <b>.N d) \<theta>n = (AndR <a>.M <b>.N d)"
-| "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL1 (x).M z) \<theta>n = (AndL1 (x).M z)"
-| "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL2 (x).M z) \<theta>n = (AndL2 (x).M z)"
-| "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR1 <a>.M b) \<theta>n = (OrR1 <a>.M b)"
-| "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR2 <a>.M b) \<theta>n = (OrR2 <a>.M b)"
-| "\<lbrakk>x\<sharp>(N,z,u,\<theta>n);u\<sharp>(M,z,x,\<theta>n)\<rbrakk> \<Longrightarrow> stn (OrL (x).M (u).N z) \<theta>n = (OrL (x).M (u).N z)"
-| "\<lbrakk>a\<sharp>(b,\<theta>n);x\<sharp>\<theta>n\<rbrakk> \<Longrightarrow> stn (ImpR (x).<a>.M b) \<theta>n = (ImpR (x).<a>.M b)"
-| "\<lbrakk>a\<sharp>(N,\<theta>n);x\<sharp>(M,z,\<theta>n)\<rbrakk> \<Longrightarrow> stn (ImpL <a>.M (x).N z) \<theta>n = (ImpL <a>.M (x).N z)"
+  "stn (Ax x a) \<theta>_n = lookupc x a \<theta>_n"
+| "\<lbrakk>a\<sharp>(N,\<theta>_n);x\<sharp>(M,\<theta>_n)\<rbrakk> \<Longrightarrow> stn (Cut <a>.M (x).N) \<theta>_n = (Cut <a>.M (x).N)" 
+| "x\<sharp>\<theta>_n \<Longrightarrow> stn (NotR (x).M a) \<theta>_n = (NotR (x).M a)"
+| "a\<sharp>\<theta>_n \<Longrightarrow>stn (NotL <a>.M x) \<theta>_n = (NotL <a>.M x)"
+| "\<lbrakk>a\<sharp>(N,d,b,\<theta>_n);b\<sharp>(M,d,a,\<theta>_n)\<rbrakk> \<Longrightarrow> stn (AndR <a>.M <b>.N d) \<theta>_n = (AndR <a>.M <b>.N d)"
+| "x\<sharp>(z,\<theta>_n) \<Longrightarrow> stn (AndL1 (x).M z) \<theta>_n = (AndL1 (x).M z)"
+| "x\<sharp>(z,\<theta>_n) \<Longrightarrow> stn (AndL2 (x).M z) \<theta>_n = (AndL2 (x).M z)"
+| "a\<sharp>(b,\<theta>_n) \<Longrightarrow> stn (OrR1 <a>.M b) \<theta>_n = (OrR1 <a>.M b)"
+| "a\<sharp>(b,\<theta>_n) \<Longrightarrow> stn (OrR2 <a>.M b) \<theta>_n = (OrR2 <a>.M b)"
+| "\<lbrakk>x\<sharp>(N,z,u,\<theta>_n);u\<sharp>(M,z,x,\<theta>_n)\<rbrakk> \<Longrightarrow> stn (OrL (x).M (u).N z) \<theta>_n = (OrL (x).M (u).N z)"
+| "\<lbrakk>a\<sharp>(b,\<theta>_n);x\<sharp>\<theta>_n\<rbrakk> \<Longrightarrow> stn (ImpR (x).<a>.M b) \<theta>_n = (ImpR (x).<a>.M b)"
+| "\<lbrakk>a\<sharp>(N,\<theta>_n);x\<sharp>(M,z,\<theta>_n)\<rbrakk> \<Longrightarrow> stn (ImpL <a>.M (x).N z) \<theta>_n = (ImpL <a>.M (x).N z)"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh abs_supp fin_supp)+
 apply(fresh_guess)+
 done
 
-nominal_primrec (freshness_context: "\<theta>c::(coname\<times>name\<times>trm)")
+nominal_primrec (freshness_context: "\<theta>_c::(coname\<times>name\<times>trm)")
   stc :: "trm\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm" 
 where
-  "stc (Ax x a) \<theta>c = lookupd x a \<theta>c"
-| "\<lbrakk>a\<sharp>(N,\<theta>c);x\<sharp>(M,\<theta>c)\<rbrakk> \<Longrightarrow> stc (Cut <a>.M (x).N) \<theta>c = (Cut <a>.M (x).N)" 
-| "x\<sharp>\<theta>c \<Longrightarrow> stc (NotR (x).M a) \<theta>c = (NotR (x).M a)"
-| "a\<sharp>\<theta>c \<Longrightarrow> stc (NotL <a>.M x) \<theta>c = (NotL <a>.M x)"
-| "\<lbrakk>a\<sharp>(N,d,b,\<theta>c);b\<sharp>(M,d,a,\<theta>c)\<rbrakk> \<Longrightarrow> stc (AndR <a>.M <b>.N d) \<theta>c = (AndR <a>.M <b>.N d)"
-| "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL1 (x).M z) \<theta>c = (AndL1 (x).M z)"
-| "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL2 (x).M z) \<theta>c = (AndL2 (x).M z)"
-| "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR1 <a>.M b) \<theta>c = (OrR1 <a>.M b)"
-| "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR2 <a>.M b) \<theta>c = (OrR2 <a>.M b)"
-| "\<lbrakk>x\<sharp>(N,z,u,\<theta>c);u\<sharp>(M,z,x,\<theta>c)\<rbrakk> \<Longrightarrow> stc (OrL (x).M (u).N z) \<theta>c = (OrL (x).M (u).N z)"
-| "\<lbrakk>a\<sharp>(b,\<theta>c);x\<sharp>\<theta>c\<rbrakk> \<Longrightarrow> stc (ImpR (x).<a>.M b) \<theta>c = (ImpR (x).<a>.M b)"
-| "\<lbrakk>a\<sharp>(N,\<theta>c);x\<sharp>(M,z,\<theta>c)\<rbrakk> \<Longrightarrow> stc (ImpL <a>.M (x).N z) \<theta>c = (ImpL <a>.M (x).N z)"
+  "stc (Ax x a) \<theta>_c = lookupd x a \<theta>_c"
+| "\<lbrakk>a\<sharp>(N,\<theta>_c);x\<sharp>(M,\<theta>_c)\<rbrakk> \<Longrightarrow> stc (Cut <a>.M (x).N) \<theta>_c = (Cut <a>.M (x).N)" 
+| "x\<sharp>\<theta>_c \<Longrightarrow> stc (NotR (x).M a) \<theta>_c = (NotR (x).M a)"
+| "a\<sharp>\<theta>_c \<Longrightarrow> stc (NotL <a>.M x) \<theta>_c = (NotL <a>.M x)"
+| "\<lbrakk>a\<sharp>(N,d,b,\<theta>_c);b\<sharp>(M,d,a,\<theta>_c)\<rbrakk> \<Longrightarrow> stc (AndR <a>.M <b>.N d) \<theta>_c = (AndR <a>.M <b>.N d)"
+| "x\<sharp>(z,\<theta>_c) \<Longrightarrow> stc (AndL1 (x).M z) \<theta>_c = (AndL1 (x).M z)"
+| "x\<sharp>(z,\<theta>_c) \<Longrightarrow> stc (AndL2 (x).M z) \<theta>_c = (AndL2 (x).M z)"
+| "a\<sharp>(b,\<theta>_c) \<Longrightarrow> stc (OrR1 <a>.M b) \<theta>_c = (OrR1 <a>.M b)"
+| "a\<sharp>(b,\<theta>_c) \<Longrightarrow> stc (OrR2 <a>.M b) \<theta>_c = (OrR2 <a>.M b)"
+| "\<lbrakk>x\<sharp>(N,z,u,\<theta>_c);u\<sharp>(M,z,x,\<theta>_c)\<rbrakk> \<Longrightarrow> stc (OrL (x).M (u).N z) \<theta>_c = (OrL (x).M (u).N z)"
+| "\<lbrakk>a\<sharp>(b,\<theta>_c);x\<sharp>\<theta>_c\<rbrakk> \<Longrightarrow> stc (ImpR (x).<a>.M b) \<theta>_c = (ImpR (x).<a>.M b)"
+| "\<lbrakk>a\<sharp>(N,\<theta>_c);x\<sharp>(M,z,\<theta>_c)\<rbrakk> \<Longrightarrow> stc (ImpL <a>.M (x).N z) \<theta>_c = (ImpL <a>.M (x).N z)"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh abs_supp fin_supp)+
@@ -3571,33 +3571,33 @@
 lemma stn_eqvt[eqvt]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
-  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)"
+  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.strong_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.strong_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
 
 lemma stc_eqvt[eqvt]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
-  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)"
+  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.strong_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.strong_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
 
 lemma stn_fresh:
   fixes a::"coname"
   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.strong_induct)
+  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.strong_induct)
 apply(auto simp add: abs_fresh fresh_prod fresh_atm)
 apply(rule lookupc_freshness)
 apply(simp add: fresh_atm)
@@ -3608,9 +3608,9 @@
 lemma stc_fresh:
   fixes a::"coname"
   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.strong_induct)
+  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.strong_induct)
 apply(auto simp add: abs_fresh fresh_prod fresh_atm)
 apply(rule lookupd_freshness)
 apply(simp add: fresh_atm)
@@ -3652,58 +3652,58 @@
 apply(perm_simp)
 done
 
-nominal_primrec (freshness_context: "(\<theta>n::(name\<times>coname\<times>trm) list,\<theta>c::(coname\<times>name\<times>trm) list)")
+nominal_primrec (freshness_context: "(\<theta>_n::(name\<times>coname\<times>trm) list,\<theta>_c::(coname\<times>name\<times>trm) list)")
   psubst :: "(name\<times>coname\<times>trm) list\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm\<Rightarrow>trm" ("_,_<_>" [100,100,100] 100) 
 where
-  "\<theta>n,\<theta>c<Ax x a> = lookup x a \<theta>n \<theta>c" 
-| "\<lbrakk>a\<sharp>(N,\<theta>n,\<theta>c);x\<sharp>(M,\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> \<theta>n,\<theta>c<Cut <a>.M (x).N> = 
-   Cut <a>.(if \<exists>x. M=Ax x a then stn M \<theta>n else \<theta>n,\<theta>c<M>) 
-       (x).(if \<exists>a. N=Ax x a then stc N \<theta>c else \<theta>n,\<theta>c<N>)" 
-| "x\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotR (x).M a> = 
-  (case (findc \<theta>c a) of 
-       Some (u,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.NotR (x).(\<theta>n,\<theta>c<M>) a' (u).P) 
-     | None \<Rightarrow> NotR (x).(\<theta>n,\<theta>c<M>) a)"
-| "a\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotL <a>.M x> = 
-  (case (findn \<theta>n x) of 
-       Some (c,P) \<Rightarrow> fresh_fun (\<lambda>x'. Cut <c>.P (x').(NotL <a>.(\<theta>n,\<theta>c<M>) x')) 
-     | None \<Rightarrow> NotL <a>.(\<theta>n,\<theta>c<M>) x)"
-| "\<lbrakk>a\<sharp>(N,c,\<theta>n,\<theta>c);b\<sharp>(M,c,\<theta>n,\<theta>c);b\<noteq>a\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<AndR <a>.M <b>.N c>) = 
-  (case (findc \<theta>c c) of 
-       Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.(AndR <a>.(\<theta>n,\<theta>c<M>) <b>.(\<theta>n,\<theta>c<N>) a') (x).P)
-     | None \<Rightarrow> AndR <a>.(\<theta>n,\<theta>c<M>) <b>.(\<theta>n,\<theta>c<N>) c)"
-| "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL1 (x).M z>) = 
-  (case (findn \<theta>n z) of 
-       Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).(\<theta>n,\<theta>c<M>) z') 
-     | None \<Rightarrow> AndL1 (x).(\<theta>n,\<theta>c<M>) z)"
-| "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL2 (x).M z>) = 
-  (case (findn \<theta>n z) of 
-       Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).(\<theta>n,\<theta>c<M>) z') 
-     | None \<Rightarrow> AndL2 (x).(\<theta>n,\<theta>c<M>) z)"
-| "\<lbrakk>x\<sharp>(N,z,\<theta>n,\<theta>c);u\<sharp>(M,z,\<theta>n,\<theta>c);x\<noteq>u\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<OrL (x).M (u).N z>) =
-  (case (findn \<theta>n z) of  
-       Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').OrL (x).(\<theta>n,\<theta>c<M>) (u).(\<theta>n,\<theta>c<N>) z') 
-     | None \<Rightarrow> OrL (x).(\<theta>n,\<theta>c<M>) (u).(\<theta>n,\<theta>c<N>) z)"
-| "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR1 <a>.M b>) = 
-  (case (findc \<theta>c b) of
-       Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.OrR1 <a>.(\<theta>n,\<theta>c<M>) a' (x).P) 
-     | None \<Rightarrow> OrR1 <a>.(\<theta>n,\<theta>c<M>) b)"
-| "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR2 <a>.M b>) = 
-  (case (findc \<theta>c b) of
-       Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.OrR2 <a>.(\<theta>n,\<theta>c<M>) a' (x).P) 
-     | None \<Rightarrow> OrR2 <a>.(\<theta>n,\<theta>c<M>) b)"
-| "\<lbrakk>a\<sharp>(b,\<theta>n,\<theta>c); x\<sharp>(\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<ImpR (x).<a>.M b>) = 
-  (case (findc \<theta>c b) of
-       Some (z,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.(\<theta>n,\<theta>c<M>) a' (z).P)
-     | None \<Rightarrow> ImpR (x).<a>.(\<theta>n,\<theta>c<M>) b)"
-| "\<lbrakk>a\<sharp>(N,\<theta>n,\<theta>c); x\<sharp>(z,M,\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<ImpL <a>.M (x).N z>) = 
-  (case (findn \<theta>n z) of
-       Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.(\<theta>n,\<theta>c<M>) (x).(\<theta>n,\<theta>c<N>) z') 
-     | None \<Rightarrow> ImpL <a>.(\<theta>n,\<theta>c<M>) (x).(\<theta>n,\<theta>c<N>) z)"
+  "\<theta>_n,\<theta>_c<Ax x a> = lookup x a \<theta>_n \<theta>_c" 
+| "\<lbrakk>a\<sharp>(N,\<theta>_n,\<theta>_c);x\<sharp>(M,\<theta>_n,\<theta>_c)\<rbrakk> \<Longrightarrow> \<theta>_n,\<theta>_c<Cut <a>.M (x).N> = 
+   Cut <a>.(if \<exists>x. M=Ax x a then stn M \<theta>_n else \<theta>_n,\<theta>_c<M>) 
+       (x).(if \<exists>a. N=Ax x a then stc N \<theta>_c else \<theta>_n,\<theta>_c<N>)" 
+| "x\<sharp>(\<theta>_n,\<theta>_c) \<Longrightarrow> \<theta>_n,\<theta>_c<NotR (x).M a> = 
+  (case (findc \<theta>_c a) of 
+       Some (u,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.NotR (x).(\<theta>_n,\<theta>_c<M>) a' (u).P) 
+     | None \<Rightarrow> NotR (x).(\<theta>_n,\<theta>_c<M>) a)"
+| "a\<sharp>(\<theta>_n,\<theta>_c) \<Longrightarrow> \<theta>_n,\<theta>_c<NotL <a>.M x> = 
+  (case (findn \<theta>_n x) of 
+       Some (c,P) \<Rightarrow> fresh_fun (\<lambda>x'. Cut <c>.P (x').(NotL <a>.(\<theta>_n,\<theta>_c<M>) x')) 
+     | None \<Rightarrow> NotL <a>.(\<theta>_n,\<theta>_c<M>) x)"
+| "\<lbrakk>a\<sharp>(N,c,\<theta>_n,\<theta>_c);b\<sharp>(M,c,\<theta>_n,\<theta>_c);b\<noteq>a\<rbrakk> \<Longrightarrow> (\<theta>_n,\<theta>_c<AndR <a>.M <b>.N c>) = 
+  (case (findc \<theta>_c c) of 
+       Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.(AndR <a>.(\<theta>_n,\<theta>_c<M>) <b>.(\<theta>_n,\<theta>_c<N>) a') (x).P)
+     | None \<Rightarrow> AndR <a>.(\<theta>_n,\<theta>_c<M>) <b>.(\<theta>_n,\<theta>_c<N>) c)"
+| "x\<sharp>(z,\<theta>_n,\<theta>_c) \<Longrightarrow> (\<theta>_n,\<theta>_c<AndL1 (x).M z>) = 
+  (case (findn \<theta>_n z) of 
+       Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).(\<theta>_n,\<theta>_c<M>) z') 
+     | None \<Rightarrow> AndL1 (x).(\<theta>_n,\<theta>_c<M>) z)"
+| "x\<sharp>(z,\<theta>_n,\<theta>_c) \<Longrightarrow> (\<theta>_n,\<theta>_c<AndL2 (x).M z>) = 
+  (case (findn \<theta>_n z) of 
+       Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).(\<theta>_n,\<theta>_c<M>) z') 
+     | None \<Rightarrow> AndL2 (x).(\<theta>_n,\<theta>_c<M>) z)"
+| "\<lbrakk>x\<sharp>(N,z,\<theta>_n,\<theta>_c);u\<sharp>(M,z,\<theta>_n,\<theta>_c);x\<noteq>u\<rbrakk> \<Longrightarrow> (\<theta>_n,\<theta>_c<OrL (x).M (u).N z>) =
+  (case (findn \<theta>_n z) of  
+       Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').OrL (x).(\<theta>_n,\<theta>_c<M>) (u).(\<theta>_n,\<theta>_c<N>) z') 
+     | None \<Rightarrow> OrL (x).(\<theta>_n,\<theta>_c<M>) (u).(\<theta>_n,\<theta>_c<N>) z)"
+| "a\<sharp>(b,\<theta>_n,\<theta>_c) \<Longrightarrow> (\<theta>_n,\<theta>_c<OrR1 <a>.M b>) = 
+  (case (findc \<theta>_c b) of
+       Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.OrR1 <a>.(\<theta>_n,\<theta>_c<M>) a' (x).P) 
+     | None \<Rightarrow> OrR1 <a>.(\<theta>_n,\<theta>_c<M>) b)"
+| "a\<sharp>(b,\<theta>_n,\<theta>_c) \<Longrightarrow> (\<theta>_n,\<theta>_c<OrR2 <a>.M b>) = 
+  (case (findc \<theta>_c b) of
+       Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.OrR2 <a>.(\<theta>_n,\<theta>_c<M>) a' (x).P) 
+     | None \<Rightarrow> OrR2 <a>.(\<theta>_n,\<theta>_c<M>) b)"
+| "\<lbrakk>a\<sharp>(b,\<theta>_n,\<theta>_c); x\<sharp>(\<theta>_n,\<theta>_c)\<rbrakk> \<Longrightarrow> (\<theta>_n,\<theta>_c<ImpR (x).<a>.M b>) = 
+  (case (findc \<theta>_c b) of
+       Some (z,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.(\<theta>_n,\<theta>_c<M>) a' (z).P)
+     | None \<Rightarrow> ImpR (x).<a>.(\<theta>_n,\<theta>_c<M>) b)"
+| "\<lbrakk>a\<sharp>(N,\<theta>_n,\<theta>_c); x\<sharp>(z,M,\<theta>_n,\<theta>_c)\<rbrakk> \<Longrightarrow> (\<theta>_n,\<theta>_c<ImpL <a>.M (x).N z>) = 
+  (case (findn \<theta>_n z) of
+       Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.(\<theta>_n,\<theta>_c<M>) (x).(\<theta>_n,\<theta>_c<N>) z') 
+     | None \<Rightarrow> ImpL <a>.(\<theta>_n,\<theta>_c<M>) (x).(\<theta>_n,\<theta>_c<N>) z)"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh stc_fresh)
 apply(simp add: abs_fresh stn_fresh)
-apply(case_tac "findc \<theta>c x3")
+apply(case_tac "findc \<theta>_c x3")
 apply(simp add: abs_fresh)
 apply(auto)[1]
 apply(generate_fresh "coname")
@@ -3711,7 +3711,7 @@
 apply(drule cmaps_fresh)
 apply(auto simp add: fresh_prod)[1]
 apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findn \<theta>n x3")
+apply(case_tac "findn \<theta>_n x3")
 apply(simp add: abs_fresh)
 apply(auto)[1]
 apply(generate_fresh "name")
@@ -3719,7 +3719,7 @@
 apply(drule nmaps_fresh)
 apply(auto simp add: fresh_prod)[1]
 apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findc \<theta>c x5")
+apply(case_tac "findc \<theta>_c x5")
 apply(simp add: abs_fresh)
 apply(auto)[1]
 apply(generate_fresh "coname")
@@ -3727,7 +3727,7 @@
 apply(drule cmaps_fresh)
 apply(auto simp add: fresh_prod)[1]
 apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findc \<theta>c x5")
+apply(case_tac "findc \<theta>_c x5")
 apply(simp add: abs_fresh)
 apply(auto)[1]
 apply(generate_fresh "coname")
@@ -3735,7 +3735,7 @@
 apply(drule_tac x="x3" in cmaps_fresh)
 apply(auto simp add: fresh_prod)[1]
 apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findn \<theta>n x3")
+apply(case_tac "findn \<theta>_n x3")
 apply(simp add: abs_fresh)
 apply(auto)[1]
 apply(generate_fresh "name")
@@ -3743,7 +3743,7 @@
 apply(drule nmaps_fresh)
 apply(auto simp add: fresh_prod)[1]
 apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findn \<theta>n x3")
+apply(case_tac "findn \<theta>_n x3")
 apply(simp add: abs_fresh)
 apply(auto)[1]
 apply(generate_fresh "name")
@@ -3751,7 +3751,7 @@
 apply(drule nmaps_fresh)
 apply(auto simp add: fresh_prod)[1]
 apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findc \<theta>c x3")
+apply(case_tac "findc \<theta>_c x3")
 apply(simp add: abs_fresh)
 apply(auto)[1]
 apply(generate_fresh "coname")
@@ -3759,7 +3759,7 @@
 apply(drule cmaps_fresh)
 apply(auto simp add: fresh_prod)[1]
 apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findc \<theta>c x3")
+apply(case_tac "findc \<theta>_c x3")
 apply(simp add: abs_fresh)
 apply(auto)[1]
 apply(generate_fresh "coname")
@@ -3767,7 +3767,7 @@
 apply(drule cmaps_fresh)
 apply(auto simp add: fresh_prod)[1]
 apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findn \<theta>n x5")
+apply(case_tac "findn \<theta>_n x5")
 apply(simp add: abs_fresh)
 apply(auto)[1]
 apply(generate_fresh "name")
@@ -3775,7 +3775,7 @@
 apply(drule nmaps_fresh)
 apply(auto simp add: fresh_prod)[1]
 apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findn \<theta>n x5")
+apply(case_tac "findn \<theta>_n x5")
 apply(simp add: abs_fresh)
 apply(auto)[1]
 apply(generate_fresh "name")
@@ -3783,7 +3783,7 @@
 apply(drule_tac a="x3" in nmaps_fresh)
 apply(auto simp add: fresh_prod)[1]
 apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findc \<theta>c x4")
+apply(case_tac "findc \<theta>_c x4")
 apply(simp add: abs_fresh abs_supp fin_supp)
 apply(auto)[1]
 apply(generate_fresh "coname")
@@ -3791,7 +3791,7 @@
 apply(drule cmaps_fresh)
 apply(auto simp add: fresh_prod)[1]
 apply(simp add: abs_fresh fresh_prod fresh_atm abs_supp fin_supp)
-apply(case_tac "findc \<theta>c x4")
+apply(case_tac "findc \<theta>_c x4")
 apply(simp add: abs_fresh abs_supp fin_supp)
 apply(auto)[1]
 apply(generate_fresh "coname")
@@ -3799,7 +3799,7 @@
 apply(drule_tac x="x2" in cmaps_fresh)
 apply(auto simp add: fresh_prod)[1]
 apply(simp add: abs_fresh fresh_prod fresh_atm abs_supp fin_supp)
-apply(case_tac "findn \<theta>n x5")
+apply(case_tac "findn \<theta>_n x5")
 apply(simp add: abs_fresh)
 apply(auto)[1]
 apply(generate_fresh "name")
@@ -3807,7 +3807,7 @@
 apply(drule nmaps_fresh)
 apply(auto simp add: fresh_prod)[1]
 apply(simp add: abs_fresh fresh_prod fresh_atm)
-apply(case_tac "findn \<theta>n x5")
+apply(case_tac "findn \<theta>_n x5")
 apply(simp add: abs_fresh)
 apply(auto)[1]
 apply(generate_fresh "name")
@@ -3826,17 +3826,17 @@
 done
 
 lemma find_maps:
-  shows "\<theta>c cmaps a to (findc \<theta>c a)"
-  and   "\<theta>n nmaps x to (findn \<theta>n x)"
+  shows "\<theta>_c cmaps a to (findc \<theta>_c a)"
+  and   "\<theta>_n nmaps x to (findn \<theta>_n x)"
 apply(auto)
 done
 
 lemma psubst_eqvt[eqvt]:
   fixes pi1::"name prm"
   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.strong_induct)
+  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.strong_induct)
 apply(auto simp add: eq_bij fresh_bij eqvts perm_pi_simp)
 apply(rule case_cong)
 apply(rule find_maps)
@@ -3921,69 +3921,69 @@
 done
 
 lemma ax_psubst:
-  assumes a: "\<theta>n,\<theta>c<M> = Ax x a"
-  and     b: "a\<sharp>(\<theta>n,\<theta>c)" "x\<sharp>(\<theta>n,\<theta>c)"
+  assumes a: "\<theta>_n,\<theta>_c<M> = Ax x a"
+  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.strong_induct)
+apply(nominal_induct M avoiding: \<theta>_n \<theta>_c rule: trm.strong_induct)
 apply(auto)
 apply(drule lookup_unicity)
 apply(simp)+
-apply(case_tac "findc \<theta>c coname")
+apply(case_tac "findc \<theta>_c coname")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp)
-apply(case_tac "findn \<theta>n name")
+apply(case_tac "findn \<theta>_n name")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "name")
 apply(fresh_fun_simp)
 apply(simp)
-apply(case_tac "findc \<theta>c coname3")
+apply(case_tac "findc \<theta>_c coname3")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "name")
 apply(fresh_fun_simp)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "name")
 apply(fresh_fun_simp)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp)
-apply(case_tac "findn \<theta>n name3")
+apply(case_tac "findn \<theta>_n name3")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "name")
 apply(fresh_fun_simp)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "name")
@@ -4113,10 +4113,10 @@
 
 lemma psubst_fresh_name:
   fixes x::"name"
-  assumes a: "x\<sharp>\<theta>n" "x\<sharp>\<theta>c" "x\<sharp>M"
-  shows "x\<sharp>\<theta>n,\<theta>c<M>"
+  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.strong_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)
@@ -4126,70 +4126,70 @@
 apply(simp add: lookupd_freshness)
 apply(simp add: lookupc_freshness)
 apply(simp)
-apply(case_tac "findc \<theta>c coname")
+apply(case_tac "findc \<theta>_c coname")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
 apply(simp)
-apply(case_tac "findn \<theta>n name")
+apply(case_tac "findn \<theta>_n name")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "name")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
 apply(simp)
-apply(case_tac "findc \<theta>c coname3")
+apply(case_tac "findc \<theta>_c coname3")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "name")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "name")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
 apply(simp)
-apply(case_tac "findn \<theta>n name3")
+apply(case_tac "findn \<theta>_n name3")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "name")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(auto simp add: abs_fresh abs_supp fin_supp)[1]
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh abs_supp fin_supp fresh_prod fresh_atm cmaps_fresh)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "name")
@@ -4199,10 +4199,10 @@
 
 lemma psubst_fresh_coname:
   fixes a::"coname"
-  assumes a: "a\<sharp>\<theta>n" "a\<sharp>\<theta>c" "a\<sharp>M"
-  shows "a\<sharp>\<theta>n,\<theta>c<M>"
+  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.strong_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)
@@ -4212,70 +4212,70 @@
 apply(simp add: lookupc_freshness)
 apply(simp add: lookupd_freshness)
 apply(simp)
-apply(case_tac "findc \<theta>c coname")
+apply(case_tac "findc \<theta>_c coname")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
 apply(simp)
-apply(case_tac "findn \<theta>n name")
+apply(case_tac "findn \<theta>_n name")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "name")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
 apply(simp)
-apply(case_tac "findc \<theta>c coname3")
+apply(case_tac "findc \<theta>_c coname3")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "name")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "name")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm cmaps_fresh)
 apply(simp)
-apply(case_tac "findn \<theta>n name3")
+apply(case_tac "findn \<theta>_n name3")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "name")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh fresh_prod fresh_atm nmaps_fresh)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(auto simp add: abs_fresh abs_supp fin_supp)[1]
 apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh abs_supp fin_supp fresh_prod fresh_atm cmaps_fresh)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(auto simp add: abs_fresh)[1]
 apply(auto)[1]
 apply(generate_fresh "name")
@@ -4284,10 +4284,10 @@
 done
 
 lemma psubst_csubst:
-  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})"
+  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.strong_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)
@@ -4298,7 +4298,7 @@
 apply(simp)
 apply(simp add: abs_fresh fresh_atm)
 apply(simp add: lookupd_fresh)
-apply(subgoal_tac "a\<sharp>lookupc xa coname \<theta>n")
+apply(subgoal_tac "a\<sharp>lookupc xa coname \<theta>_n")
 apply(simp add: forget)
 apply(simp add: trm.inject)
 apply(rule sym)
@@ -4315,8 +4315,8 @@
 apply(rule impI)
 apply(simp add: lookupd_unicity)
 apply(rule impI)
-apply(subgoal_tac "a\<sharp>lookupc xa coname \<theta>n")
-apply(subgoal_tac "a\<sharp>lookupd name aa \<theta>c")
+apply(subgoal_tac "a\<sharp>lookupc xa coname \<theta>_n")
+apply(subgoal_tac "a\<sharp>lookupd name aa \<theta>_c")
 apply(simp add: forget)
 apply(rule lookupd_freshness)
 apply(simp add: fresh_atm)
@@ -4335,7 +4335,7 @@
 apply(simp)
 apply(blast)
 apply(rule impI)
-apply(subgoal_tac "a\<sharp>lookupc xa coname \<theta>n")
+apply(subgoal_tac "a\<sharp>lookupc xa coname \<theta>_n")
 apply(simp add: forget)
 apply(rule lookupc_freshness)
 apply(simp add: fresh_atm)
@@ -4362,7 +4362,7 @@
 apply(rule impI)
 apply(simp add: lookupd_unicity)
 apply(rule impI)
-apply(subgoal_tac "a\<sharp>lookupd name aa \<theta>c")
+apply(subgoal_tac "a\<sharp>lookupd name aa \<theta>_c")
 apply(simp add: forget)
 apply(rule lookupd_freshness)
 apply(simp add: fresh_atm)
@@ -4379,7 +4379,7 @@
 apply(blast)
 (* NotR *)
 apply(simp)
-apply(case_tac "findc \<theta>c coname")
+apply(case_tac "findc \<theta>_c coname")
 apply(simp)
 apply(auto simp add: fresh_list_cons fresh_prod)[1]
 apply(simp)
@@ -4398,7 +4398,7 @@
 apply(auto simp add: fresh_prod fresh_atm)[1]
 (* NotL *)
 apply(simp)
-apply(case_tac "findn \<theta>n name")
+apply(case_tac "findn \<theta>_n name")
 apply(simp)
 apply(auto simp add: fresh_list_cons fresh_prod)[1]
 apply(simp)
@@ -4417,7 +4417,7 @@
 apply(simp)
 (* AndR *)
 apply(simp)
-apply(case_tac "findc \<theta>c coname3")
+apply(case_tac "findc \<theta>_c coname3")
 apply(simp)
 apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
 apply(simp)
@@ -4436,7 +4436,7 @@
 apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
 (* AndL1 *)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(simp)
 apply(auto simp add: fresh_list_cons fresh_prod)[1]
 apply(simp)
@@ -4455,7 +4455,7 @@
 apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
 (* AndL2 *)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(simp)
 apply(auto simp add: fresh_list_cons fresh_prod)[1]
 apply(simp)
@@ -4474,7 +4474,7 @@
 apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
 (* OrR1 *)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(simp)
 apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
 apply(simp)
@@ -4493,7 +4493,7 @@
 apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
 (* OrR2 *)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(simp)
 apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
 apply(simp)
@@ -4512,7 +4512,7 @@
 apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
 (* OrL *)
 apply(simp)
-apply(case_tac "findn \<theta>n name3")
+apply(case_tac "findn \<theta>_n name3")
 apply(simp)
 apply(auto simp add: fresh_list_cons psubst_fresh_name fresh_atm fresh_prod)[1]
 apply(simp)
@@ -4531,7 +4531,7 @@
 apply(auto simp add:  psubst_fresh_name fresh_prod fresh_atm)[1]
 (* ImpR *)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(simp)
 apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
 apply(simp)
@@ -4550,7 +4550,7 @@
 apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
 (* ImpL *)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(simp)
 apply(auto simp add: fresh_list_cons psubst_fresh_coname psubst_fresh_name fresh_atm fresh_prod)[1]
 apply(simp)
@@ -4571,10 +4571,10 @@
 done
 
 lemma psubst_nsubst:
-  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})"
+  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.strong_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)
@@ -4591,7 +4591,7 @@
 apply(simp add: abs_fresh)
 apply(simp add: abs_fresh fresh_atm)
 apply(simp add: lookupd_fresh)
-apply(subgoal_tac "x\<sharp>lookupd name aa \<theta>c")
+apply(subgoal_tac "x\<sharp>lookupd name aa \<theta>_c")
 apply(simp add: forget)
 apply(simp add: trm.inject)
 apply(rule sym)
@@ -4608,8 +4608,8 @@
 apply(rule impI)
 apply(simp add: lookupc_unicity)
 apply(rule impI)
-apply(subgoal_tac "x\<sharp>lookupc xa coname \<theta>n")
-apply(subgoal_tac "x\<sharp>lookupd name aa \<theta>c")
+apply(subgoal_tac "x\<sharp>lookupc xa coname \<theta>_n")
+apply(subgoal_tac "x\<sharp>lookupd name aa \<theta>_c")
 apply(simp add: forget)
 apply(rule lookupd_freshness)
 apply(simp add: fresh_atm)
@@ -4638,7 +4638,7 @@
 apply(rule impI)
 apply(simp add: lookupc_unicity)
 apply(rule impI)
-apply(subgoal_tac "x\<sharp>lookupc xa coname \<theta>n")
+apply(subgoal_tac "x\<sharp>lookupc xa coname \<theta>_n")
 apply(simp add: forget)
 apply(rule lookupc_freshness)
 apply(simp add: fresh_prod fresh_atm)
@@ -4656,7 +4656,7 @@
 apply(simp)
 apply(blast)
 apply(rule impI)
-apply(subgoal_tac "x\<sharp>lookupd name aa \<theta>c")
+apply(subgoal_tac "x\<sharp>lookupd name aa \<theta>_c")
 apply(simp add: forget)
 apply(rule lookupd_freshness)
 apply(simp add: fresh_atm)
@@ -4673,7 +4673,7 @@
 apply(blast)
 (* NotR *)
 apply(simp)
-apply(case_tac "findc \<theta>c coname")
+apply(case_tac "findc \<theta>_c coname")
 apply(simp)
 apply(auto simp add: fresh_list_cons fresh_prod)[1]
 apply(simp)
@@ -4690,7 +4690,7 @@
 apply(simp)
 (* NotL *)
 apply(simp)
-apply(case_tac "findn \<theta>n name")
+apply(case_tac "findn \<theta>_n name")
 apply(simp)
 apply(auto simp add: fresh_list_cons fresh_prod)[1]
 apply(simp)
@@ -4709,7 +4709,7 @@
 apply(simp add: fresh_prod fresh_atm)
 (* AndR *)
 apply(simp)
-apply(case_tac "findc \<theta>c coname3")
+apply(case_tac "findc \<theta>_c coname3")
 apply(simp)
 apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
 apply(simp)
@@ -4726,7 +4726,7 @@
 apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
 (* AndL1 *)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(simp)
 apply(auto simp add: fresh_list_cons fresh_prod)[1]
 apply(simp)
@@ -4745,7 +4745,7 @@
 apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
 (* AndL2 *)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(simp)
 apply(auto simp add: fresh_list_cons fresh_prod)[1]
 apply(simp)
@@ -4764,7 +4764,7 @@
 apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
 (* OrR1 *)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(simp)
 apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
 apply(simp)
@@ -4781,7 +4781,7 @@
 apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
 (* OrR2 *)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(simp)
 apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
 apply(simp)
@@ -4798,7 +4798,7 @@
 apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
 (* OrL *)
 apply(simp)
-apply(case_tac "findn \<theta>n name3")
+apply(case_tac "findn \<theta>_n name3")
 apply(simp)
 apply(auto simp add: fresh_list_cons psubst_fresh_name fresh_atm fresh_prod)[1]
 apply(simp)
@@ -4817,7 +4817,7 @@
 apply(auto simp add:  psubst_fresh_name fresh_prod fresh_atm)[1]
 (* ImpR *)
 apply(simp)
-apply(case_tac "findc \<theta>c coname2")
+apply(case_tac "findc \<theta>_c coname2")
 apply(simp)
 apply(auto simp add: psubst_fresh_coname fresh_list_cons fresh_prod fresh_atm)[1]
 apply(simp)
@@ -4834,7 +4834,7 @@
 apply(auto simp add:  psubst_fresh_coname fresh_prod fresh_atm)[1]
 (* ImpL *)
 apply(simp)
-apply(case_tac "findn \<theta>n name2")
+apply(case_tac "findn \<theta>_n name2")
 apply(simp)
 apply(auto simp add: fresh_list_cons psubst_fresh_coname psubst_fresh_name fresh_atm fresh_prod)[1]
 apply(simp)
@@ -4856,35 +4856,35 @@
 definition 
   ncloses :: "(name\<times>coname\<times>trm) list\<Rightarrow>(name\<times>ty) list \<Rightarrow> bool" ("_ ncloses _" [55,55] 55) 
 where
-  "\<theta>n ncloses \<Gamma> \<equiv> \<forall>x B. ((x,B) \<in> set \<Gamma> \<longrightarrow> (\<exists>c P. \<theta>n nmaps x to Some (c,P) \<and> <c>:P \<in> (\<parallel><B>\<parallel>)))"
+  "\<theta>_n ncloses \<Gamma> \<equiv> \<forall>x B. ((x,B) \<in> set \<Gamma> \<longrightarrow> (\<exists>c P. \<theta>_n nmaps x to Some (c,P) \<and> <c>:P \<in> (\<parallel><B>\<parallel>)))"
   
 definition 
   ccloses :: "(coname\<times>name\<times>trm) list\<Rightarrow>(coname\<times>ty) list \<Rightarrow> bool" ("_ ccloses _" [55,55] 55) 
 where
-  "\<theta>c ccloses \<Delta> \<equiv> \<forall>a B. ((a,B) \<in> set \<Delta> \<longrightarrow> (\<exists>x P. \<theta>c cmaps a to Some (x,P) \<and> (x):P \<in> (\<parallel>(B)\<parallel>)))"
+  "\<theta>_c ccloses \<Delta> \<equiv> \<forall>a B. ((a,B) \<in> set \<Delta> \<longrightarrow> (\<exists>x P. \<theta>_c cmaps a to Some (x,P) \<and> (x):P \<in> (\<parallel>(B)\<parallel>)))"
 
 lemma ncloses_elim:
   assumes a: "(x,B) \<in> set \<Gamma>"
-  and     b: "\<theta>n ncloses \<Gamma>"
-  shows "\<exists>c P. \<theta>n nmaps x to Some (c,P) \<and> <c>:P \<in> (\<parallel><B>\<parallel>)"
+  and     b: "\<theta>_n ncloses \<Gamma>"
+  shows "\<exists>c P. \<theta>_n nmaps x to Some (c,P) \<and> <c>:P \<in> (\<parallel><B>\<parallel>)"
 using a b by (auto simp add: ncloses_def)
 
 lemma ccloses_elim:
   assumes a: "(a,B) \<in> set \<Delta>"
-  and     b: "\<theta>c ccloses \<Delta>"
-  shows "\<exists>x P. \<theta>c cmaps a to Some (x,P) \<and> (x):P \<in> (\<parallel>(B)\<parallel>)"
+  and     b: "\<theta>_c ccloses \<Delta>"
+  shows "\<exists>x P. \<theta>_c cmaps a to Some (x,P) \<and> (x):P \<in> (\<parallel>(B)\<parallel>)"
 using a b by (auto simp add: ccloses_def)
 
 lemma ncloses_subset:
-  assumes a: "\<theta>n ncloses \<Gamma>"
+  assumes a: "\<theta>_n ncloses \<Gamma>"
   and     b: "set \<Gamma>' \<subseteq> set \<Gamma>"
-  shows "\<theta>n ncloses \<Gamma>'"
+  shows "\<theta>_n ncloses \<Gamma>'"
 using a b by (auto  simp add: ncloses_def)
 
 lemma ccloses_subset:
-  assumes a: "\<theta>c ccloses \<Delta>"
+  assumes a: "\<theta>_c ccloses \<Delta>"
   and     b: "set \<Delta>' \<subseteq> set \<Delta>"
-  shows "\<theta>c ccloses \<Delta>'"
+  shows "\<theta>_c ccloses \<Delta>'"
 using a b by (auto  simp add: ccloses_def)
 
 lemma validc_fresh:
@@ -4908,8 +4908,8 @@
 done
 
 lemma ccloses_extend:
-  assumes a: "\<theta>c ccloses \<Delta>" "a\<sharp>\<Delta>" "a\<sharp>\<theta>c" "(x):P\<in>\<parallel>(B)\<parallel>"
-  shows "(a,x,P)#\<theta>c ccloses (a,B)#\<Delta>"
+  assumes a: "\<theta>_c ccloses \<Delta>" "a\<sharp>\<Delta>" "a\<sharp>\<theta>_c" "(x):P\<in>\<parallel>(B)\<parallel>"
+  shows "(a,x,P)#\<theta>_c ccloses (a,B)#\<Delta>"
 using a
 apply(simp add: ccloses_def)
 apply(drule validc_fresh)
@@ -4917,8 +4917,8 @@
 done
 
 lemma ncloses_extend:
-  assumes a: "\<theta>n ncloses \<Gamma>" "x\<sharp>\<Gamma>" "x\<sharp>\<theta>n" "<a>:P\<in>\<parallel><B>\<parallel>"
-  shows "(x,a,P)#\<theta>n ncloses (x,B)#\<Gamma>"
+  assumes a: "\<theta>_n ncloses \<Gamma>" "x\<sharp>\<Gamma>" "x\<sharp>\<theta>_n" "<a>:P\<in>\<parallel><B>\<parallel>"
+  shows "(x,a,P)#\<theta>_n ncloses (x,B)#\<Gamma>"
 using a
 apply(simp add: ncloses_def)
 apply(drule validn_fresh)
@@ -5082,39 +5082,39 @@
 done
 
 lemma psubst_Ax_aux: 
-  assumes a: "\<theta>c cmaps a to Some (y,N)"
-  shows "lookupb x a \<theta>c c P = Cut <c>.P (y).N"
+  assumes a: "\<theta>_c cmaps a to Some (y,N)"
+  shows "lookupb x a \<theta>_c c P = Cut <c>.P (y).N"
 using a
-apply(induct \<theta>c)
+apply(induct \<theta>_c)
 apply(auto)
 done
 
 lemma psubst_Ax:
-  assumes a: "\<theta>n nmaps x to Some (c,P)"
-  and     b: "\<theta>c cmaps a to Some (y,N)"
-  shows "\<theta>n,\<theta>c<Ax x a> = Cut <c>.P (y).N"
+  assumes a: "\<theta>_n nmaps x to Some (c,P)"
+  and     b: "\<theta>_c cmaps a to Some (y,N)"
+  shows "\<theta>_n,\<theta>_c<Ax x a> = Cut <c>.P (y).N"
 using a b
-apply(induct \<theta>n)
+apply(induct \<theta>_n)
 apply(auto simp add: psubst_Ax_aux)
 done
 
 lemma psubst_Cut:
   assumes a: "\<forall>x. M\<noteq>Ax x c"
   and     b: "\<forall>a. N\<noteq>Ax x a"
-  and     c: "c\<sharp>(\<theta>n,\<theta>c,N)" "x\<sharp>(\<theta>n,\<theta>c,M)"
-  shows "\<theta>n,\<theta>c<Cut <c>.M (x).N> = Cut <c>.(\<theta>n,\<theta>c<M>) (x).(\<theta>n,\<theta>c<N>)"
+  and     c: "c\<sharp>(\<theta>_n,\<theta>_c,N)" "x\<sharp>(\<theta>_n,\<theta>_c,M)"
+  shows "\<theta>_n,\<theta>_c<Cut <c>.M (x).N> = Cut <c>.(\<theta>_n,\<theta>_c<M>) (x).(\<theta>_n,\<theta>_c<N>)"
 using a b c
 apply(simp)
 done
 
 lemma all_CAND: 
   assumes a: "\<Gamma> \<turnstile> M \<turnstile> \<Delta>"
-  and     b: "\<theta>n ncloses \<Gamma>"
-  and     c: "\<theta>c ccloses \<Delta>"
-  shows "SNa (\<theta>n,\<theta>c<M>)"
+  and     b: "\<theta>_n ncloses \<Gamma>"
+  and     c: "\<theta>_c ccloses \<Delta>"
+  shows "SNa (\<theta>_n,\<theta>_c<M>)"
 using a b c
-proof(nominal_induct avoiding: \<theta>n \<theta>c rule: typing.strong_induct)
-  case (TAx \<Gamma> \<Delta> x B a \<theta>n \<theta>c)
+proof(nominal_induct avoiding: \<theta>_n \<theta>_c rule: typing.strong_induct)
+  case (TAx \<Gamma> \<Delta> x B a \<theta>_n \<theta>_c)
   then show ?case
     apply -
     apply(drule ncloses_elim)
@@ -5123,13 +5123,13 @@
     apply(assumption)
     apply(erule exE)+
     apply(erule conjE)+
-    apply(rule_tac s="Cut <c>.P (xa).Pa" and t="\<theta>n,\<theta>c<Ax x a>" in subst)
+    apply(rule_tac s="Cut <c>.P (xa).Pa" and t="\<theta>_n,\<theta>_c<Ax x a>" in subst)
     apply(rule sym)
     apply(simp only: psubst_Ax)
     apply(simp add: CUT_SNa)
     done
 next
-  case (TNotR x \<Gamma> B M \<Delta> \<Delta>' a \<theta>n \<theta>c) 
+  case (TNotR x \<Gamma> B M \<Delta> \<Delta>' a \<theta>_n \<theta>_c) 
   then show ?case 
     apply(simp)
     apply(subgoal_tac "(a,NOT B) \<in> set \<Delta>'")
@@ -5145,7 +5145,7 @@
     apply(rule disjI2)
     apply(rule_tac x="c" in exI)
     apply(rule_tac x="x" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp)
     apply(rule conjI)
     apply(rule fic.intros)
@@ -5157,13 +5157,13 @@
     apply(unfold BINDINGn_def)
     apply(simp)
     apply(rule_tac x="x" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp)
     apply(rule allI)+
     apply(rule impI)
     apply(simp add: psubst_nsubst[symmetric])
-    apply(drule_tac x="(x,aa,Pa)#\<theta>n" in meta_spec)
-    apply(drule_tac x="\<theta>c" in meta_spec)
+    apply(drule_tac x="(x,aa,Pa)#\<theta>_n" in meta_spec)
+    apply(drule_tac x="\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(rule ncloses_extend)
     apply(assumption)
@@ -5179,7 +5179,7 @@
     apply(blast)
     done
 next
-  case (TNotL a \<Delta> \<Gamma> M B \<Gamma>' x \<theta>n \<theta>c)
+  case (TNotL a \<Delta> \<Gamma> M B \<Gamma>' x \<theta>_n \<theta>_c)
   then show ?case
     apply(simp)
     apply(subgoal_tac "(x,NOT B) \<in> set \<Gamma>'")
@@ -5197,7 +5197,7 @@
     apply(rule disjI2)
     apply(rule_tac x="a" in exI)
     apply(rule_tac x="ca" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule conjI)
     apply(rule fin.intros)
@@ -5209,13 +5209,13 @@
     apply(unfold BINDINGc_def)
     apply(simp (no_asm))
     apply(rule_tac x="a" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp (no_asm))
     apply(rule allI)+
     apply(rule impI)
     apply(simp del: NEGc.simps add: psubst_csubst[symmetric])
-    apply(drule_tac x="\<theta>n" in meta_spec)
-    apply(drule_tac x="(a,xa,Pa)#\<theta>c" in meta_spec)
+    apply(drule_tac x="\<theta>_n" in meta_spec)
+    apply(drule_tac x="(a,xa,Pa)#\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(rule ncloses_subset)
     apply(assumption)
@@ -5230,7 +5230,7 @@
     apply(blast)
     done
 next
-  case (TAndL1 x \<Gamma> y B1 M \<Delta> \<Gamma>' B2 \<theta>n \<theta>c)
+  case (TAndL1 x \<Gamma> y B1 M \<Delta> \<Gamma>' B2 \<theta>_n \<theta>_c)
   then show ?case     
     apply(simp)
     apply(subgoal_tac "(y,B1 AND B2) \<in> set \<Gamma>'")
@@ -5249,7 +5249,7 @@
     apply(rule disjI1)
     apply(rule_tac x="x" in exI)
     apply(rule_tac x="ca" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule conjI)
     apply(rule fin.intros)
@@ -5262,13 +5262,13 @@
     apply(unfold BINDINGn_def)
     apply(simp (no_asm))
     apply(rule_tac x="x" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp (no_asm))
     apply(rule allI)+
     apply(rule impI)
     apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
-    apply(drule_tac x="(x,a,Pa)#\<theta>n" in meta_spec)
-    apply(drule_tac x="\<theta>c" in meta_spec)
+    apply(drule_tac x="(x,a,Pa)#\<theta>_n" in meta_spec)
+    apply(drule_tac x="\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(rule ncloses_extend)
     apply(rule ncloses_subset)
@@ -5283,7 +5283,7 @@
     apply(blast)
     done
 next
-  case (TAndL2 x \<Gamma> y B2 M \<Delta> \<Gamma>' B1 \<theta>n \<theta>c)
+  case (TAndL2 x \<Gamma> y B2 M \<Delta> \<Gamma>' B1 \<theta>_n \<theta>_c)
   then show ?case 
     apply(simp)
     apply(subgoal_tac "(y,B1 AND B2) \<in> set \<Gamma>'")
@@ -5302,7 +5302,7 @@
     apply(rule disjI2)
     apply(rule_tac x="x" in exI)
     apply(rule_tac x="ca" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule conjI)
     apply(rule fin.intros)
@@ -5315,13 +5315,13 @@
     apply(unfold BINDINGn_def)
     apply(simp (no_asm))
     apply(rule_tac x="x" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp (no_asm))
     apply(rule allI)+
     apply(rule impI)
     apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
-    apply(drule_tac x="(x,a,Pa)#\<theta>n" in meta_spec)
-    apply(drule_tac x="\<theta>c" in meta_spec)
+    apply(drule_tac x="(x,a,Pa)#\<theta>_n" in meta_spec)
+    apply(drule_tac x="\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(rule ncloses_extend)
     apply(rule ncloses_subset)
@@ -5336,7 +5336,7 @@
     apply(blast)
     done
 next
-  case (TAndR a \<Delta> N c b M \<Gamma> B C \<Delta>' \<theta>n \<theta>c)
+  case (TAndR a \<Delta> N c b M \<Gamma> B C \<Delta>' \<theta>_n \<theta>_c)
   then show ?case 
     apply(simp)
     apply(subgoal_tac "(c,B AND C) \<in> set \<Delta>'")
@@ -5353,8 +5353,8 @@
     apply(rule_tac x="ca" in exI)
     apply(rule_tac x="a" in exI)
     apply(rule_tac x="b" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
     apply(simp)
     apply(rule conjI)
     apply(rule fic.intros)
@@ -5373,13 +5373,13 @@
     apply(unfold BINDINGc_def)
     apply(simp)
     apply(rule_tac x="a" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp)
     apply(rule allI)+
     apply(rule impI)
     apply(simp add: psubst_csubst[symmetric])
-    apply(drule_tac x="\<theta>n" in meta_spec)
-    apply(drule_tac x="(a,xa,Pa)#\<theta>c" in meta_spec)
+    apply(drule_tac x="\<theta>_n" in meta_spec)
+    apply(drule_tac x="(a,xa,Pa)#\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(assumption)
     apply(drule meta_mp)
@@ -5395,14 +5395,14 @@
     apply(unfold BINDINGc_def)
     apply(simp)
     apply(rule_tac x="b" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
     apply(simp)
     apply(rule allI)+
     apply(rule impI)
     apply(simp add: psubst_csubst[symmetric])
     apply(rotate_tac 14)
-    apply(drule_tac x="\<theta>n" in meta_spec)
-    apply(drule_tac x="(b,xa,Pa)#\<theta>c" in meta_spec)
+    apply(drule_tac x="\<theta>_n" in meta_spec)
+    apply(drule_tac x="(b,xa,Pa)#\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(assumption)
     apply(drule meta_mp)
@@ -5418,7 +5418,7 @@
     apply(blast)
     done
 next
-  case (TOrL x \<Gamma> N z y M B \<Delta> C \<Gamma>' \<theta>n \<theta>c)
+  case (TOrL x \<Gamma> N z y M B \<Delta> C \<Gamma>' \<theta>_n \<theta>_c)
   then show ?case 
     apply(simp)
     apply(subgoal_tac "(z,B OR C) \<in> set \<Gamma>'")
@@ -5437,8 +5437,8 @@
     apply(rule_tac x="x" in exI)
     apply(rule_tac x="y" in exI)
     apply(rule_tac x="ca" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule conjI)
     apply(rule fin.intros)
@@ -5457,13 +5457,13 @@
     apply(unfold BINDINGn_def)
     apply(simp del: NEGc.simps)
     apply(rule_tac x="x" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule allI)+
     apply(rule impI)
     apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
-    apply(drule_tac x="(x,a,Pa)#\<theta>n" in meta_spec)
-    apply(drule_tac x="\<theta>c" in meta_spec)
+    apply(drule_tac x="(x,a,Pa)#\<theta>_n" in meta_spec)
+    apply(drule_tac x="\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(rule ncloses_extend)
     apply(rule ncloses_subset)
@@ -5479,14 +5479,14 @@
     apply(unfold BINDINGn_def)
     apply(simp del: NEGc.simps)
     apply(rule_tac x="y" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule allI)+
     apply(rule impI)
     apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
     apply(rotate_tac 14)
-    apply(drule_tac x="(y,a,Pa)#\<theta>n" in meta_spec)
-    apply(drule_tac x="\<theta>c" in meta_spec)
+    apply(drule_tac x="(y,a,Pa)#\<theta>_n" in meta_spec)
+    apply(drule_tac x="\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(rule ncloses_extend)
     apply(rule ncloses_subset)
@@ -5501,7 +5501,7 @@
     apply(blast)
     done
 next
-  case (TOrR1 a \<Delta> b \<Gamma> M B1 \<Delta>' B2 \<theta>n \<theta>c)
+  case (TOrR1 a \<Delta> b \<Gamma> M B1 \<Delta>' B2 \<theta>_n \<theta>_c)
   then show ?case
     apply(simp)
     apply(subgoal_tac "(b,B1 OR B2) \<in> set \<Delta>'")
@@ -5518,7 +5518,7 @@
     apply(rule disjI1)
     apply(rule_tac x="a" in exI)
     apply(rule_tac x="c" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp)
     apply(rule conjI)
     apply(rule fic.intros)
@@ -5531,13 +5531,13 @@
     apply(unfold BINDINGc_def)
     apply(simp (no_asm))
     apply(rule_tac x="a" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp (no_asm))
     apply(rule allI)+
     apply(rule impI)    
     apply(simp del: NEGc.simps add: psubst_csubst[symmetric])
-    apply(drule_tac x="\<theta>n" in meta_spec)
-    apply(drule_tac x="(a,xa,Pa)#\<theta>c" in meta_spec)
+    apply(drule_tac x="\<theta>_n" in meta_spec)
+    apply(drule_tac x="(a,xa,Pa)#\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(assumption)
     apply(drule meta_mp)
@@ -5553,7 +5553,7 @@
     apply(blast)
     done
 next
-  case (TOrR2 a \<Delta> b \<Gamma> M B2 \<Delta>' B1 \<theta>n \<theta>c)
+  case (TOrR2 a \<Delta> b \<Gamma> M B2 \<Delta>' B1 \<theta>_n \<theta>_c)
   then show ?case 
     apply(simp)
     apply(subgoal_tac "(b,B1 OR B2) \<in> set \<Delta>'")
@@ -5570,7 +5570,7 @@
     apply(rule disjI2)
     apply(rule_tac x="a" in exI)
     apply(rule_tac x="c" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp)
     apply(rule conjI)
     apply(rule fic.intros)
@@ -5583,13 +5583,13 @@
     apply(unfold BINDINGc_def)
     apply(simp (no_asm))
     apply(rule_tac x="a" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp (no_asm))
     apply(rule allI)+
     apply(rule impI)    
     apply(simp del: NEGc.simps add: psubst_csubst[symmetric])
-    apply(drule_tac x="\<theta>n" in meta_spec)
-    apply(drule_tac x="(a,xa,Pa)#\<theta>c" in meta_spec)
+    apply(drule_tac x="\<theta>_n" in meta_spec)
+    apply(drule_tac x="(a,xa,Pa)#\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(assumption)
     apply(drule meta_mp)
@@ -5605,7 +5605,7 @@
     apply(blast)
     done
 next
-  case (TImpL a \<Delta> N x \<Gamma> M y B C \<Gamma>' \<theta>n \<theta>c)
+  case (TImpL a \<Delta> N x \<Gamma> M y B C \<Gamma>' \<theta>_n \<theta>_c)
   then show ?case
     apply(simp)
     apply(subgoal_tac "(y,B IMP C) \<in> set \<Gamma>'")
@@ -5624,8 +5624,8 @@
     apply(rule_tac x="x" in exI)
     apply(rule_tac x="a" in exI)
     apply(rule_tac x="ca" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule conjI)
     apply(rule fin.intros)
@@ -5643,13 +5643,13 @@
     apply(unfold BINDINGc_def)
     apply(simp del: NEGc.simps)
     apply(rule_tac x="a" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule allI)+
     apply(rule impI)
     apply(simp del: NEGc.simps add: psubst_csubst[symmetric])
-    apply(drule_tac x="\<theta>n" in meta_spec)
-    apply(drule_tac x="(a,xa,Pa)#\<theta>c" in meta_spec)
+    apply(drule_tac x="\<theta>_n" in meta_spec)
+    apply(drule_tac x="(a,xa,Pa)#\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(rule ncloses_subset)
     apply(assumption)
@@ -5665,14 +5665,14 @@
     apply(unfold BINDINGn_def)
     apply(simp del: NEGc.simps)
     apply(rule_tac x="x" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
     apply(simp del: NEGc.simps)
     apply(rule allI)+
     apply(rule impI)
     apply(simp del: NEGc.simps add: psubst_nsubst[symmetric])
     apply(rotate_tac 12)
-    apply(drule_tac x="(x,aa,Pa)#\<theta>n" in meta_spec)
-    apply(drule_tac x="\<theta>c" in meta_spec)
+    apply(drule_tac x="(x,aa,Pa)#\<theta>_n" in meta_spec)
+    apply(drule_tac x="\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(rule ncloses_extend)
     apply(rule ncloses_subset)
@@ -5687,7 +5687,7 @@
     apply(blast)
     done
 next
-  case (TImpR a \<Delta> b x \<Gamma> B M C \<Delta>' \<theta>n \<theta>c)
+  case (TImpR a \<Delta> b x \<Gamma> B M C \<Delta>' \<theta>_n \<theta>_c)
   then show ?case
     apply(simp)
     apply(subgoal_tac "(b,B IMP C) \<in> set \<Delta>'")
@@ -5704,7 +5704,7 @@
     apply(rule_tac x="x" in exI)
     apply(rule_tac x="a" in exI)
     apply(rule_tac x="c" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp)
     apply(rule conjI)
     apply(rule fic.intros)
@@ -5721,16 +5721,16 @@
     apply(unfold BINDINGn_def)
     apply(simp)
     apply(rule_tac x="x" in exI)
-    apply(rule_tac x="\<theta>n,((a,z,Pa)#\<theta>c)<M>" in exI)
+    apply(rule_tac x="\<theta>_n,((a,z,Pa)#\<theta>_c)<M>" in exI)
     apply(simp)
     apply(rule allI)+
     apply(rule impI)
-    apply(rule_tac t="\<theta>n,((a,z,Pa)#\<theta>c)<M>{x:=<aa>.Pb}" and 
-                   s="((x,aa,Pb)#\<theta>n),((a,z,Pa)#\<theta>c)<M>" in subst)
+    apply(rule_tac t="\<theta>_n,((a,z,Pa)#\<theta>_c)<M>{x:=<aa>.Pb}" and 
+                   s="((x,aa,Pb)#\<theta>_n),((a,z,Pa)#\<theta>_c)<M>" in subst)
     apply(rule psubst_nsubst)
     apply(simp add: fresh_prod fresh_atm fresh_list_cons)
-    apply(drule_tac x="(x,aa,Pb)#\<theta>n" in meta_spec)
-    apply(drule_tac x="(a,z,Pa)#\<theta>c" in meta_spec)
+    apply(drule_tac x="(x,aa,Pb)#\<theta>_n" in meta_spec)
+    apply(drule_tac x="(a,z,Pa)#\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(rule ncloses_extend)
     apply(assumption)
@@ -5753,16 +5753,16 @@
     apply(unfold BINDINGc_def)
     apply(simp)
     apply(rule_tac x="a" in exI)
-    apply(rule_tac x="((x,ca,Q)#\<theta>n),\<theta>c<M>" in exI)
+    apply(rule_tac x="((x,ca,Q)#\<theta>_n),\<theta>_c<M>" in exI)
     apply(simp)
     apply(rule allI)+
     apply(rule impI)
-    apply(rule_tac t="((x,ca,Q)#\<theta>n),\<theta>c<M>{a:=(xaa).Pa}" and 
-                   s="((x,ca,Q)#\<theta>n),((a,xaa,Pa)#\<theta>c)<M>" in subst)
+    apply(rule_tac t="((x,ca,Q)#\<theta>_n),\<theta>_c<M>{a:=(xaa).Pa}" and 
+                   s="((x,ca,Q)#\<theta>_n),((a,xaa,Pa)#\<theta>_c)<M>" in subst)
     apply(rule psubst_csubst)
     apply(simp add: fresh_prod fresh_atm fresh_list_cons)
-    apply(drule_tac x="(x,ca,Q)#\<theta>n" in meta_spec)
-    apply(drule_tac x="(a,xaa,Pa)#\<theta>c" in meta_spec)
+    apply(drule_tac x="(x,ca,Q)#\<theta>_n" in meta_spec)
+    apply(drule_tac x="(a,xaa,Pa)#\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(rule ncloses_extend)
     apply(assumption)
@@ -5782,7 +5782,7 @@
     apply(blast)
     done
 next
-  case (TCut a \<Delta> N x \<Gamma> M B \<theta>n \<theta>c)
+  case (TCut a \<Delta> N x \<Gamma> M B \<theta>_n \<theta>_c)
   then show ?case 
     apply -
     apply(case_tac "\<forall>y. M\<noteq>Ax y a")
@@ -5793,14 +5793,14 @@
     apply(unfold BINDINGc_def)
     apply(simp)
     apply(rule_tac x="a" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp)
     apply(rule allI)
     apply(rule allI)
     apply(rule impI)
     apply(simp add: psubst_csubst[symmetric]) (*?*)
-    apply(drule_tac x="\<theta>n" in meta_spec)
-    apply(drule_tac x="(a,xa,P)#\<theta>c" in meta_spec)
+    apply(drule_tac x="\<theta>_n" in meta_spec)
+    apply(drule_tac x="(a,xa,P)#\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(assumption)
     apply(drule meta_mp)
@@ -5814,15 +5814,15 @@
     apply(unfold BINDINGn_def)
     apply(simp)
     apply(rule_tac x="x" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
     apply(simp)
     apply(rule allI)
     apply(rule allI)
     apply(rule impI)
     apply(simp add: psubst_nsubst[symmetric]) (*?*)
     apply(rotate_tac 11)
-    apply(drule_tac x="(x,aa,P)#\<theta>n" in meta_spec)
-    apply(drule_tac x="\<theta>c" in meta_spec)
+    apply(drule_tac x="(x,aa,P)#\<theta>_n" in meta_spec)
+    apply(drule_tac x="\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(rule ncloses_extend)
     apply(assumption)
@@ -5844,12 +5844,12 @@
     apply(unfold BINDINGc_def)
     apply(simp)
     apply(rule_tac x="a" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<M>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<M>" in exI)
     apply(simp)
     apply(rule allI)+
     apply(rule impI)
-    apply(drule_tac x="\<theta>n" in meta_spec)
-    apply(drule_tac x="(a,xa,P)#\<theta>c" in meta_spec)
+    apply(drule_tac x="\<theta>_n" in meta_spec)
+    apply(drule_tac x="(a,xa,P)#\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(assumption)
     apply(drule meta_mp)
@@ -5935,15 +5935,15 @@
     apply(unfold BINDINGn_def)
     apply(simp)
     apply(rule_tac x="x" in exI)
-    apply(rule_tac x="\<theta>n,\<theta>c<N>" in exI)
+    apply(rule_tac x="\<theta>_n,\<theta>_c<N>" in exI)
     apply(simp)
     apply(rule allI)
     apply(rule allI)
     apply(rule impI)
     apply(simp add: psubst_nsubst[symmetric]) (*?*)
     apply(rotate_tac 10)
-    apply(drule_tac x="(x,aa,P)#\<theta>n" in meta_spec)
-    apply(drule_tac x="\<theta>c" in meta_spec)
+    apply(drule_tac x="(x,aa,P)#\<theta>_n" in meta_spec)
+    apply(drule_tac x="\<theta>_c" in meta_spec)
     apply(drule meta_mp)
     apply(rule ncloses_extend)
     apply(assumption)
@@ -6038,7 +6038,7 @@
 
 lemma lookup1:
   assumes a: "x\<sharp>(idn \<Gamma> b)"
-  shows "lookup x a (idn \<Gamma> b) \<theta>c = lookupa x a \<theta>c"
+  shows "lookup x a (idn \<Gamma> b) \<theta>_c = lookupa x a \<theta>_c"
 using a
 apply(induct \<Gamma>)
 apply(auto simp add: fresh_list_cons fresh_prod fresh_atm)
@@ -6046,7 +6046,7 @@
 
 lemma lookup2:
   assumes a: "\<not>(x\<sharp>(idn \<Gamma> b))"
-  shows "lookup x a (idn \<Gamma> b) \<theta>c = lookupb x a \<theta>c b (Ax x b)"
+  shows "lookup x a (idn \<Gamma> b) \<theta>_c = lookupb x a \<theta>_c b (Ax x b)"
 using a
 apply(induct \<Gamma>)
 apply(auto simp add: fresh_list_cons fresh_prod fresh_atm fresh_list_nil)
diff -r 227477f17c26 -r 4aa34bd43228 src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Wed Nov 28 15:38:12 2012 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Wed Nov 28 15:59:18 2012 +0100
@@ -1501,7 +1501,7 @@
   have h:"(D @ TVarB X Q # \<Gamma>)\<turnstile>S<:T" by fact
   then have ST: "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S[X \<mapsto> P]\<^sub>\<tau> <: T[X \<mapsto> P]\<^sub>\<tau>" using SA_trans_TVar by auto
   from h have G_ok: "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by (rule subtype_implies_ok)
-  from G_ok and SA_trans_TVar have X\<Gamma>_ok: "\<turnstile> (TVarB X Q # \<Gamma>) ok"
+  from G_ok and SA_trans_TVar have X_\<Gamma>_ok: "\<turnstile> (TVarB X Q # \<Gamma>) ok"
     by (auto intro: validE_append)
   show "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> Tvar Y[X \<mapsto> P]\<^sub>\<tau><:T[X \<mapsto> P]\<^sub>\<tau>"
   proof (cases "X = Y")
@@ -1509,7 +1509,7 @@
     from eq and SA_trans_TVar have "TVarB Y Q \<in> set (D @ TVarB X Q # \<Gamma>)" by simp
     with G_ok have QS: "Q = S" using `TVarB Y S \<in> set (D @ TVarB X Q # \<Gamma>)`
       by (rule uniqueness_of_ctxt)
-    from X\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "Q closed_in \<Gamma>" by auto
+    from X_\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "Q closed_in \<Gamma>" by auto
     then have XQ: "X \<sharp> Q" by (rule closed_in_fresh)
     note `\<Gamma>\<turnstile>P<:Q`
     moreover from ST have "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" by (rule subtype_implies_ok)
@@ -1534,7 +1534,7 @@
       with neq and ST show ?thesis by auto
     next
       assume Y: "TVarB Y S \<in> set \<Gamma>"
-      from X\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "\<turnstile> \<Gamma> ok" by auto
+      from X_\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "\<turnstile> \<Gamma> ok" by auto
       then have "X \<sharp> \<Gamma>" by (simp add: valid_ty_dom_fresh)
       with Y have "X \<sharp> S"
         by (induct \<Gamma>) (auto simp add: fresh_list_nil fresh_list_cons)
diff -r 227477f17c26 -r 4aa34bd43228 src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Nov 28 15:38:12 2012 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Nov 28 15:59:18 2012 +0100
@@ -19,8 +19,10 @@
   assume "\<not> finite I"
   then have I_not_empty: "I \<noteq> {}" by auto
   interpret G!: algebra ?\<Omega> generator by (rule algebra_generator) fact
-  note \<mu>G_mono =
-    G.additive_increasing[OF positive_\<mu>G[OF I_not_empty] additive_\<mu>G[OF I_not_empty], THEN increasingD]
+  note mu_G_mono =
+    G.additive_increasing[OF positive_mu_G[OF I_not_empty] additive_mu_G[OF I_not_empty],
+      THEN increasingD]
+  write mu_G  ("\<mu>G")
 
   { fix Z J assume J: "J \<noteq> {}" "finite J" "J \<subseteq> I" and Z: "Z \<in> ?G"
 
@@ -42,7 +44,7 @@
       have ***: "((\<lambda>x. merge J (I - J) (y, x)) -` Z \<inter> space (Pi\<^isub>M I M)) \<in> ?G"
         using J K by (intro generatorI) auto
       have "\<mu>G ((\<lambda>x. merge J (I - J) (y, x)) -` emb I K X \<inter> space (Pi\<^isub>M I M)) = emeasure (Pi\<^isub>M (K - J) M) (?M y)"
-        unfolding * using K J by (subst \<mu>G_eq[OF _ _ _ **]) auto
+        unfolding * using K J by (subst mu_G_eq[OF _ _ _ **]) auto
       note * ** *** this }
     note merge_in_G = this
 
@@ -61,7 +63,7 @@
       fix x assume x: "x \<in> space (Pi\<^isub>M J M)"
       with K merge_in_G(2)[OF this]
       show "emeasure (Pi\<^isub>M (K - J) M) (?M x) = \<mu>G (?MZ x)"
-        unfolding `Z = emb I K X` merge_in_G(1)[OF x] by (subst \<mu>G_eq) auto
+        unfolding `Z = emb I K X` merge_in_G(1)[OF x] by (subst mu_G_eq) auto
     qed
     finally have fold: "\<mu>G Z = (\<integral>\<^isup>+x. \<mu>G (?MZ x) \<partial>Pi\<^isub>M J M)" .
 
@@ -74,12 +76,12 @@
     let ?q = "\<lambda>y. \<mu>G ((\<lambda>x. merge J (I - J) (y,x)) -` Z \<inter> space (Pi\<^isub>M I M))"
     have "?q \<in> borel_measurable (Pi\<^isub>M J M)"
       unfolding `Z = emb I K X` using J K merge_in_G(3)
-      by (simp add: merge_in_G  \<mu>G_eq emeasure_fold_measurable cong: measurable_cong)
+      by (simp add: merge_in_G  mu_G_eq emeasure_fold_measurable cong: measurable_cong)
     note this fold le_1 merge_in_G(3) }
   note fold = this
 
   have "\<exists>\<mu>. (\<forall>s\<in>?G. \<mu> s = \<mu>G s) \<and> measure_space ?\<Omega> (sigma_sets ?\<Omega> ?G) \<mu>"
-  proof (rule G.caratheodory_empty_continuous[OF positive_\<mu>G additive_\<mu>G])
+  proof (rule G.caratheodory_empty_continuous[OF positive_mu_G additive_mu_G])
     fix A assume "A \<in> ?G"
     with generatorE guess J X . note JX = this
     interpret JK: finite_product_prob_space M J by default fact+ 
@@ -87,13 +89,13 @@
   next
     fix A assume A: "range A \<subseteq> ?G" "decseq A" "(\<Inter>i. A i) = {}"
     then have "decseq (\<lambda>i. \<mu>G (A i))"
-      by (auto intro!: \<mu>G_mono simp: decseq_def)
+      by (auto intro!: mu_G_mono simp: decseq_def)
     moreover
     have "(INF i. \<mu>G (A i)) = 0"
     proof (rule ccontr)
       assume "(INF i. \<mu>G (A i)) \<noteq> 0" (is "?a \<noteq> 0")
       moreover have "0 \<le> ?a"
-        using A positive_\<mu>G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def)
+        using A positive_mu_G[OF I_not_empty] by (auto intro!: INF_greatest simp: positive_def)
       ultimately have "0 < ?a" by auto
 
       have "\<forall>n. \<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A n = emb I J X \<and> \<mu>G (A n) = emeasure (limP J M (\<lambda>J. (Pi\<^isub>M J M))) X"
@@ -114,7 +116,7 @@
       interpret J: finite_product_prob_space M "J i" for i by default fact+
 
       have a_le_1: "?a \<le> 1"
-        using \<mu>G_spec[of "J 0" "A 0" "X 0"] J A_eq
+        using mu_G_spec[of "J 0" "A 0" "X 0"] J A_eq
         by (auto intro!: INF_lower2[of 0] J.measure_le_1)
 
       let ?M = "\<lambda>K Z y. (\<lambda>x. merge K (I - K) (y, x)) -` Z \<inter> space (Pi\<^isub>M I M)"
@@ -166,7 +168,7 @@
             fix x assume x: "x \<in> space (Pi\<^isub>M J' M)"
             assume "?a / 2^(k+1) \<le> ?q n x"
             also have "?q n x \<le> ?q m x"
-            proof (rule \<mu>G_mono)
+            proof (rule mu_G_mono)
               from fold(4)[OF J', OF Z_sets x]
               show "?M J' (Z n) x \<in> ?G" "?M J' (Z m) x \<in> ?G" by auto
               show "?M J' (Z n) x \<subseteq> ?M J' (Z m) x"
@@ -248,7 +250,7 @@
         moreover
         from w have "?a / 2 ^ (k + 1) \<le> ?q k k (w k)" by auto
         then have "?M (J k) (A k) (w k) \<noteq> {}"
-          using positive_\<mu>G[OF I_not_empty, unfolded positive_def] `0 < ?a` `?a \<le> 1`
+          using positive_mu_G[OF I_not_empty, unfolded positive_def] `0 < ?a` `?a \<le> 1`
           by (cases ?a) (auto simp: divide_le_0_iff power_le_zero_eq)
         then obtain x where "x \<in> ?M (J k) (A k) (w k)" by auto
         then have "merge (J k) (I - J k) (w k, x) \<in> A k" by auto
@@ -317,7 +319,7 @@
     then have "\<mu> (emb I J (Pi\<^isub>E J X)) = \<mu>G (emb I J (Pi\<^isub>E J X))"
       using \<mu> by simp
     also have "\<dots> = (\<Prod> j\<in>J. if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"
-      using J  `I \<noteq> {}` by (subst \<mu>G_spec[OF _ _ _ refl]) (auto simp: emeasure_PiM Pi_iff)
+      using J  `I \<noteq> {}` by (subst mu_G_spec[OF _ _ _ refl]) (auto simp: emeasure_PiM Pi_iff)
     also have "\<dots> = (\<Prod>j\<in>J \<union> {i \<in> I. emeasure (M i) (space (M i)) \<noteq> 1}.
       if j \<in> J then emeasure (M j) (X j) else emeasure (M j) (space (M j)))"
       using J `I \<noteq> {}` by (intro setprod_mono_one_right) (auto simp: M.emeasure_space_1)
diff -r 227477f17c26 -r 4aa34bd43228 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Nov 28 15:38:12 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Nov 28 15:59:18 2012 +0100
@@ -788,7 +788,7 @@
   fix g assume g: "simple_function M g" "g \<le> max 0 \<circ> f"
   let ?G = "{x \<in> space M. \<not> g x \<noteq> \<infinity>}"
   note gM = g(1)[THEN borel_measurable_simple_function]
-  have \<mu>G_pos: "0 \<le> (emeasure M) ?G" using gM by auto
+  have \<mu>_G_pos: "0 \<le> (emeasure M) ?G" using gM by auto
   let ?g = "\<lambda>y x. if g x = \<infinity> then y else max 0 (g x)"
   from g gM have g_in_A: "\<And>y. 0 \<le> y \<Longrightarrow> y \<noteq> \<infinity> \<Longrightarrow> ?g y \<in> ?A"
     apply (safe intro!: simple_function_max simple_function_If)
@@ -804,15 +804,15 @@
       by (intro SUP_upper2[OF g0] simple_integral_mono_AE)
          (auto simp: max_def intro!: simple_function_If)
   next
-    assume \<mu>G: "(emeasure M) ?G \<noteq> 0"
+    assume \<mu>_G: "(emeasure M) ?G \<noteq> 0"
     have "SUPR ?A (integral\<^isup>S M) = \<infinity>"
     proof (intro SUP_PInfty)
       fix n :: nat
       let ?y = "ereal (real n) / (if (emeasure M) ?G = \<infinity> then 1 else (emeasure M) ?G)"
-      have "0 \<le> ?y" "?y \<noteq> \<infinity>" using \<mu>G \<mu>G_pos by (auto simp: ereal_divide_eq)
+      have "0 \<le> ?y" "?y \<noteq> \<infinity>" using \<mu>_G \<mu>_G_pos by (auto simp: ereal_divide_eq)
       then have "?g ?y \<in> ?A" by (rule g_in_A)
       have "real n \<le> ?y * (emeasure M) ?G"
-        using \<mu>G \<mu>G_pos by (cases "(emeasure M) ?G") (auto simp: field_simps)
+        using \<mu>_G \<mu>_G_pos by (cases "(emeasure M) ?G") (auto simp: field_simps)
       also have "\<dots> = (\<integral>\<^isup>Sx. ?y * indicator ?G x \<partial>M)"
         using `0 \<le> ?y` `?g ?y \<in> ?A` gM
         by (subst simple_integral_cmult_indicator) auto
diff -r 227477f17c26 -r 4aa34bd43228 src/HOL/Probability/Projective_Family.thy
--- a/src/HOL/Probability/Projective_Family.thy	Wed Nov 28 15:38:12 2012 +0100
+++ b/src/HOL/Probability/Projective_Family.thy	Wed Nov 28 15:59:18 2012 +0100
@@ -226,14 +226,14 @@
   "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> A = emb I J X \<Longrightarrow> A \<in> generator"
   unfolding generator_def by auto
 
-definition
+definition mu_G ("\<mu>G") where
   "\<mu>G A =
     (THE x. \<forall>J. J \<noteq> {} \<longrightarrow> finite J \<longrightarrow> J \<subseteq> I \<longrightarrow> (\<forall>X\<in>sets (Pi\<^isub>M J M). A = emb I J X \<longrightarrow> x = emeasure (limP J M P) X))"
 
-lemma \<mu>G_spec:
+lemma mu_G_spec:
   assumes J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)"
   shows "\<mu>G A = emeasure (limP J M P) X"
-  unfolding \<mu>G_def
+  unfolding mu_G_def
 proof (intro the_equality allI impI ballI)
   fix K Y assume K: "K \<noteq> {}" "finite K" "K \<subseteq> I" "A = emb I K Y" "Y \<in> sets (Pi\<^isub>M K M)"
   have "emeasure (limP K M P) Y = emeasure (limP (K \<union> J) M P) (emb (K \<union> J) K Y)"
@@ -245,9 +245,9 @@
   finally show "emeasure (limP J M P) X = emeasure (limP K M P) Y" ..
 qed (insert J, force)
 
-lemma \<mu>G_eq:
+lemma mu_G_eq:
   "J \<noteq> {} \<Longrightarrow> finite J \<Longrightarrow> J \<subseteq> I \<Longrightarrow> X \<in> sets (Pi\<^isub>M J M) \<Longrightarrow> \<mu>G (emb I J X) = emeasure (limP J M P) X"
-  by (intro \<mu>G_spec) auto
+  by (intro mu_G_spec) auto
 
 lemma generator_Ex:
   assumes *: "A \<in> generator"
@@ -255,7 +255,7 @@
 proof -
   from * obtain J X where J: "J \<noteq> {}" "finite J" "J \<subseteq> I" "A = emb I J X" "X \<in> sets (Pi\<^isub>M J M)"
     unfolding generator_def by auto
-  with \<mu>G_spec[OF this] show ?thesis by auto
+  with mu_G_spec[OF this] show ?thesis by auto
 qed
 
 lemma generatorE:
@@ -284,7 +284,7 @@
        auto
 qed
 
-lemma positive_\<mu>G:
+lemma positive_mu_G:
   assumes "I \<noteq> {}"
   shows "positive generator \<mu>G"
 proof -
@@ -302,7 +302,7 @@
   qed
 qed
 
-lemma additive_\<mu>G:
+lemma additive_mu_G:
   assumes "I \<noteq> {}"
   shows "additive generator \<mu>G"
 proof -
@@ -324,7 +324,7 @@
     then have "\<mu>G (A \<union> B) = \<mu>G (emb I (J \<union> K) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y))"
       by simp
     also have "\<dots> = emeasure (limP (J \<union> K) M P) (emb (J \<union> K) J X \<union> emb (J \<union> K) K Y)"
-      using JK J(1, 4) K(1, 4) by (simp add: \<mu>G_eq sets.Un del: prod_emb_Un)
+      using JK J(1, 4) K(1, 4) by (simp add: mu_G_eq sets.Un del: prod_emb_Un)
     also have "\<dots> = \<mu>G A + \<mu>G B"
       using J K JK_disj by (simp add: plus_emeasure[symmetric])
     finally show "\<mu>G (A \<union> B) = \<mu>G A + \<mu>G B" .
diff -r 227477f17c26 -r 4aa34bd43228 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Wed Nov 28 15:38:12 2012 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Wed Nov 28 15:59:18 2012 +0100
@@ -115,10 +115,13 @@
   let ?\<Omega> = "\<Pi>\<^isub>E i\<in>I. space borel"
   let ?G = generator
   interpret G!: algebra ?\<Omega> generator by (intro  algebra_generator) fact
-  note \<mu>G_mono =
-    G.additive_increasing[OF positive_\<mu>G[OF `I \<noteq> {}`] additive_\<mu>G[OF `I \<noteq> {}`], THEN increasingD]
+  note mu_G_mono =
+    G.additive_increasing[OF positive_mu_G[OF `I \<noteq> {}`] additive_mu_G[OF `I \<noteq> {}`],
+      THEN increasingD]
+  write mu_G  ("\<mu>G")
+
   have "\<exists>\<mu>. (\<forall>s\<in>?G. \<mu> s = \<mu>G s) \<and> measure_space ?\<Omega> (sigma_sets ?\<Omega> ?G) \<mu>"
-  proof (rule G.caratheodory_empty_continuous[OF positive_\<mu>G additive_\<mu>G,
+  proof (rule G.caratheodory_empty_continuous[OF positive_mu_G additive_mu_G,
       OF `I \<noteq> {}`, OF `I \<noteq> {}`])
     fix A assume "A \<in> ?G"
     with generatorE guess J X . note JX = this
@@ -127,13 +130,13 @@
   next
     fix Z assume Z: "range Z \<subseteq> ?G" "decseq Z" "(\<Inter>i. Z i) = {}"
     then have "decseq (\<lambda>i. \<mu>G (Z i))"
-      by (auto intro!: \<mu>G_mono simp: decseq_def)
+      by (auto intro!: mu_G_mono simp: decseq_def)
     moreover
     have "(INF i. \<mu>G (Z i)) = 0"
     proof (rule ccontr)
       assume "(INF i. \<mu>G (Z i)) \<noteq> 0" (is "?a \<noteq> 0")
       moreover have "0 \<le> ?a"
-        using Z positive_\<mu>G[OF `I \<noteq> {}`] by (auto intro!: INF_greatest simp: positive_def)
+        using Z positive_mu_G[OF `I \<noteq> {}`] by (auto intro!: INF_greatest simp: positive_def)
       ultimately have "0 < ?a" by auto
       hence "?a \<noteq> -\<infinity>" by auto
       have "\<forall>n. \<exists>J B. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> B \<in> sets (Pi\<^isub>M J (\<lambda>_. borel)) \<and>
@@ -158,10 +161,10 @@
         unfolding J_def B_def by (subst prod_emb_trans) (insert Z, auto)
       interpret prob_space "P (J i)" for i using proj_prob_space by simp
       have "?a \<le> \<mu>G (Z 0)" by (auto intro: INF_lower)
-      also have "\<dots> < \<infinity>" using J by (auto simp: Z_eq \<mu>G_eq limP_finite proj_sets)
+      also have "\<dots> < \<infinity>" using J by (auto simp: Z_eq mu_G_eq limP_finite proj_sets)
       finally have "?a \<noteq> \<infinity>" by simp
       have "\<And>n. \<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>" unfolding Z_eq using J J_mono
-        by (subst \<mu>G_eq) (auto simp: limP_finite proj_sets \<mu>G_eq)
+        by (subst mu_G_eq) (auto simp: limP_finite proj_sets mu_G_eq)
 
       have countable_UN_J: "countable (\<Union>n. J n)" by (simp add: countable_finite)
       def Utn \<equiv> "to_nat_on (\<Union>n. J n)"
@@ -295,7 +298,7 @@
             (\<Inter> i\<in>{1..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))" .
         hence "Y n \<in> ?G" using J J_mono K_sets `n \<ge> 1` by (intro generatorI[OF _ _ _ _ Y_emb]) auto
         hence "\<bar>\<mu>G (Y n)\<bar> \<noteq> \<infinity>" unfolding Y_emb using J J_mono K_sets `n \<ge> 1`
-          by (subst \<mu>G_eq) (auto simp: limP_finite proj_sets \<mu>G_eq)
+          by (subst mu_G_eq) (auto simp: limP_finite proj_sets mu_G_eq)
         interpret finite_measure "(limP (J n) (\<lambda>_. borel) P)"
         proof
           have "emeasure (limP (J n) (\<lambda>_. borel) P) (J n \<rightarrow>\<^isub>E space borel) \<noteq> \<infinity>"
@@ -304,14 +307,14 @@
              by (simp add: space_PiM)
         qed
         have "\<mu>G (Z n) = limP (J n) (\<lambda>_. borel) P (B n)"
-          unfolding Z_eq using J by (auto simp: \<mu>G_eq)
+          unfolding Z_eq using J by (auto simp: mu_G_eq)
         moreover have "\<mu>G (Y n) =
           limP (J n) (\<lambda>_. borel) P (\<Inter>i\<in>{Suc 0..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i))"
-          unfolding Y_emb using J J_mono K_sets `n \<ge> 1` by (subst \<mu>G_eq) auto
+          unfolding Y_emb using J J_mono K_sets `n \<ge> 1` by (subst mu_G_eq) auto
         moreover have "\<mu>G (Z n - Y n) = limP (J n) (\<lambda>_. borel) P
           (B n - (\<Inter>i\<in>{Suc 0..n}. prod_emb (J n) (\<lambda>_. borel) (J i) (K i)))"
           unfolding Z_eq Y_emb prod_emb_Diff[symmetric] using J J_mono K_sets `n \<ge> 1`
-          by (subst \<mu>G_eq) (auto intro!: sets.Diff)
+          by (subst mu_G_eq) (auto intro!: sets.Diff)
         ultimately
         have "\<mu>G (Z n) - \<mu>G (Y n) = \<mu>G (Z n - Y n)"
           using J J_mono K_sets `n \<ge> 1`
@@ -324,17 +327,17 @@
         have "Z n - Y n \<in> ?G" "(\<Union> i\<in>{1..n}. (Z i - Z' i)) \<in> ?G"
           using `Z' _ \<in> ?G` `Z _ \<in> ?G` `Y _ \<in> ?G` by auto
         hence "\<mu>G (Z n - Y n) \<le> \<mu>G (\<Union> i\<in>{1..n}. (Z i - Z' i))"
-          using subs G.additive_increasing[OF positive_\<mu>G[OF `I \<noteq> {}`] additive_\<mu>G[OF `I \<noteq> {}`]]
+          using subs G.additive_increasing[OF positive_mu_G[OF `I \<noteq> {}`] additive_mu_G[OF `I \<noteq> {}`]]
           unfolding increasing_def by auto
         also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. \<mu>G (Z i - Z' i))" using `Z _ \<in> ?G` `Z' _ \<in> ?G`
-          by (intro G.subadditive[OF positive_\<mu>G additive_\<mu>G, OF `I \<noteq> {}` `I \<noteq> {}`]) auto
+          by (intro G.subadditive[OF positive_mu_G additive_mu_G, OF `I \<noteq> {}` `I \<noteq> {}`]) auto
         also have "\<dots> \<le> (\<Sum> i\<in>{1..n}. 2 powr -real i * ?a)"
         proof (rule setsum_mono)
           fix i assume "i \<in> {1..n}" hence "i \<le> n" by simp
           have "\<mu>G (Z i - Z' i) = \<mu>G (prod_emb I (\<lambda>_. borel) (J i) (B i - K i))"
             unfolding Z'_def Z_eq by simp
           also have "\<dots> = P (J i) (B i - K i)"
-            apply (subst \<mu>G_eq) using J K_sets apply auto
+            apply (subst mu_G_eq) using J K_sets apply auto
             apply (subst limP_finite) apply auto
             done
           also have "\<dots> = P (J i) (B i) - P (J i) (K i)"
@@ -374,7 +377,7 @@
           apply (rule ereal_less_add[OF _ R]) using `\<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>` by auto
         finally have "\<mu>G (Y n) > 0"
           using `\<bar>\<mu>G (Z n)\<bar> \<noteq> \<infinity>` by (auto simp: ac_simps zero_ereal_def[symmetric])
-        thus "Y n \<noteq> {}" using positive_\<mu>G `I \<noteq> {}` by (auto simp add: positive_def)
+        thus "Y n \<noteq> {}" using positive_mu_G `I \<noteq> {}` by (auto simp add: positive_def)
       qed
       hence "\<forall>n\<in>{1..}. \<exists>y. y \<in> Y n" by auto
       then obtain y where y: "\<And>n. n \<ge> 1 \<Longrightarrow> y n \<in> Y n" unfolding bchoice_iff by force
@@ -532,7 +535,7 @@
     hence "\<mu> (emb I J (Pi\<^isub>E J X)) = \<mu>G (emb I J (Pi\<^isub>E J X))" using \<mu> by simp
     also have "\<dots> = emeasure (P J) (Pi\<^isub>E J X)"
       using JX assms proj_sets
-      by (subst \<mu>G_eq) (auto simp: \<mu>G_eq limP_finite intro: sets_PiM_I_finite)
+      by (subst mu_G_eq) (auto simp: mu_G_eq limP_finite intro: sets_PiM_I_finite)
     finally show "\<mu> (emb I J (Pi\<^isub>E J X)) = emeasure (P J) (Pi\<^isub>E J X)" .
   next
     show "emeasure (P J) (Pi\<^isub>E J B) = emeasure (limP J (\<lambda>_. borel) P) (Pi\<^isub>E J B)"
diff -r 227477f17c26 -r 4aa34bd43228 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Nov 28 15:38:12 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Wed Nov 28 15:59:18 2012 +0100
@@ -387,7 +387,7 @@
 subsection {* Binary Unions *}
 
 definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a"
-  where "binary a b =  (\<lambda>\<^isup>x. b)(0 := a)"
+  where "binary a b =  (\<lambda>x. b)(0 := a)"
 
 lemma range_binary_eq: "range(binary a b) = {a,b}"
   by (auto simp add: binary_def)
@@ -2117,7 +2117,7 @@
 subsection {* A Two-Element Series *}
 
 definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set "
-  where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)"
+  where "binaryset A B = (\<lambda>x. {})(0 := A, Suc 0 := B)"
 
 lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
   apply (simp add: binaryset_def)