--- a/Nominal/Ex/Classical.thy	Sat Dec 17 17:03:01 2011 +0000
+++ b/Nominal/Ex/Classical.thy	Sat Dec 17 17:08:47 2011 +0000
@@ -385,52 +385,6 @@
 thm crename.eqvt nrename.eqvt
 
 
-nominal_primrec 
-  substn :: "trm \<Rightarrow> name   \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) 
-where
-  "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" 
-| "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){y:=<c>.P} = 
-    (if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))" 
-| "atom x\<sharp> (y, P) \<Longrightarrow> (NotR (x).M a){y:=<c>.P} = NotR (x).(M{y:=<c>.P}) a" 
-| "\<lbrakk>atom a\<sharp> (c, P); atom x' \<sharp> (M, y, P)\<rbrakk> \<Longrightarrow> (NotL <a>.M x){y:=<c>.P} = 
-    (if x=y then Cut <c>.P (x').NotL <a>.(M{y:=<c>.P}) x' else NotL <a>.(M{y:=<c>.P}) x)"
-| "\<lbrakk>atom a \<sharp> (c, P); atom b \<sharp> (c, P)\<rbrakk> \<Longrightarrow> 
-    (AndR <a>.M <b>.N d){y:=<c>.P} = AndR <a>.(M{y:=<c>.P}) <b>.(N{y:=<c>.P}) d" 
-| "atom x \<sharp> (y, P) \<Longrightarrow> (AndL1 (x).M z){y:=<c>.P} = 
-    (if z=y then Cut <c>.P (z').AndL1 (x).(M{y:=<c>.P}) z' else AndL1 (x).(M{y:=<c>.P}) z)"
-| "atom x \<sharp> (y, P) \<Longrightarrow> (AndL2 (x).M z){y:=<c>.P} = 
-    (if z=y then Cut <c>.P (z').AndL2 (x).(M{y:=<c>.P}) z' else AndL2 (x).(M{y:=<c>.P}) z)"
-| "atom a \<sharp> (c, P) \<Longrightarrow> (OrR1 <a>.M b){y:=<c>.P} = OrR1 <a>.(M{y:=<c>.P}) b"
-| "atom a \<sharp> (c, P) \<Longrightarrow> (OrR2 <a>.M b){y:=<c>.P} = OrR2 <a>.(M{y:=<c>.P}) b"
-| "\<lbrakk>atom x \<sharp> (y, P); atom u \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (OrL (x).M (u).N z){y:=<c>.P} = 
-     (if z=y then Cut <c>.P (z').OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z' 
-      else OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z)"
-| "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){y:=<c>.P} = ImpR (x).<a>.(M{y:=<c>.P}) b"
-| "\<lbrakk>atom a \<sharp> (c, P); atom x \<sharp> (y, P)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N z){y:=<c>.P} = 
-     (if y=z then Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z' 
-      else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)"
-  apply(simp only: eqvt_def)
-  apply(simp only: substn_graph_def)
-  apply (rule, perm_simp, rule)
-  apply(rule TrueI)
-  -- "covered all cases"
-  apply(case_tac x)
-  apply(rule_tac y="a" and c="(b, c, d)" in trm.strong_exhaust)
-  apply (simp_all add: fresh_star_def fresh_Pair)[12]
-  apply(metis)+
-  apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)")
-  apply(auto simp add: fresh_Pair)[1]
-  apply(metis)+
-  apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)")
-  apply(auto simp add: fresh_Pair)[1]
-  apply(rule obtain_fresh)
-  apply(auto)[1]
-  apply(metis)+
-  -- "compatibility"
-  apply(all_trivials)
-  apply(simp)
-  oops
-
 end