--- a/Nominal/Test.thy	Mon Mar 08 15:01:26 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 08 15:06:14 2010 +0100
@@ -14,111 +14,6 @@
 thm alpha_weird_raw.intros[no_vars]
 thm fv_weird_raw.simps[no_vars]
 
-thm eqvts
-
-local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding weird_inj}, []), (build_alpha_inj @{thms alpha_weird_raw.intros} @{thms weird_raw.distinct weird_raw.inject} @{thms alpha_weird_raw.cases} ctxt)) ctxt)) *}
-thm weird_inj
-
-(*local_setup {*
-(fn ctxt => snd (Local_Theory.note ((@{binding alpha_eqvt}, []),
-build_alpha_eqvts [@{term alpha_weird_raw}] [@{term "permute :: perm \<Rightarrow> weird_raw \<Rightarrow> weird_raw"}] @{thms permute_weird_raw.simps weird_inj} @{thm alpha_weird_raw.induct} ctxt) ctxt)) *}
-
-(*prove {* (snd o snd) (build_alpha_refl_gl [@{term alpha_weird_raw}] ("x","y","z")) *}
-
-apply (tactic {* transp_tac @{context} @{thm alpha_weird_raw.induct} @{thms weird_inj}  @{thms weird_raw.inject} @{thms weird_raw.distinct} @{thms alpha_weird_raw.cases} @{thms alpha_eqvt} 1 *})
-*)
-lemma "alpha_weird_raw x y \<longrightarrow> (\<forall>z. alpha_weird_raw y z \<longrightarrow> alpha_weird_raw x z)"
-apply (rule impI)
-apply (erule alpha_weird_raw.induct)
-apply (simp_all add: weird_inj)
-defer
-apply (rule allI)
-apply (rule impI)
-apply (erule alpha_weird_raw.cases)
-apply (simp_all add: weird_inj)
-apply (rule allI)
-apply (rule impI)
-apply (erule alpha_weird_raw.cases)
-apply (simp_all add: weird_inj)
-apply (erule conjE)+
-apply (erule exE)+
-apply (erule conjE)+
-apply (erule exE)+
-apply (rule conjI)
-apply (rule_tac x="pica + pic" in exI)
-apply (erule alpha_gen_compose_trans)
-apply assumption
-apply (simp add: alpha_eqvt)
-apply (rule_tac x="pia + pib" in exI)
-apply (rule_tac x="piaa + piba" in exI)
-apply (rule conjI)
-apply (erule alpha_gen_compose_trans)
-apply assumption
-apply (simp add: alpha_eqvt)
-apply (rule conjI)
-defer
-apply (rule_tac x="pid + pi" in exI)
-apply (erule alpha_gen_compose_trans)
-apply assumption
-apply (simp add: alpha_eqvt)
-sorry
-
-lemma "alpha_weird_raw x y \<Longrightarrow> alpha_weird_raw y x"
-apply (erule alpha_weird_raw.induct)
-apply (simp_all add: weird_inj)
-apply (erule conjE)+
-apply (erule exE)+
-apply (erule conjE)+
-apply (erule exE)+
-apply (rule conjI)
-apply (rule_tac x="- pic" in exI)
-apply (erule alpha_gen_compose_sym)
-apply (simp_all add: alpha_eqvt)
-apply (rule_tac x="- pia" in exI)
-apply (rule_tac x="- pib" in exI)
-apply (simp add: minus_add[symmetric])
-apply (rule conjI)
-apply (erule alpha_gen_compose_sym)
-apply (simp_all add: alpha_eqvt)
-apply (rule conjI)
-apply (simp add: supp_minus_perm Int_commute)
-apply (rule_tac x="- pi" in exI)
-apply (erule alpha_gen_compose_sym)
-apply (simp_all add: alpha_eqvt)
-done
-
-
-abbreviation "WBind \<equiv> WBind_raw"
-abbreviation "WP \<equiv> WP_raw"
-abbreviation "WV \<equiv> WV_raw"
-
-lemma test:
-  assumes a: "distinct [x, y, z]"
-  shows "alpha_weird_raw (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y)))  
-                         (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))"
-apply(rule_tac alpha_weird_raw.intros)
-unfolding alpha_gen
-using a
-apply(auto)
-apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply(auto)
-apply(simp add: fresh_star_def flip_def fresh_def supp_swap)
-apply(rule alpha_weird_raw.intros)
-apply(simp add: alpha_weird_raw.intros(2))
-apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply(rule_tac x="0" in exI)
-apply(simp add: fresh_star_def)
-apply(auto)
-apply(rule alpha_weird_raw.intros)
-apply(simp add: alpha_weird_raw.intros(2))
-apply(simp add: flip_def supp_swap supp_perm)
-apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
-apply(simp)
-apply(auto)
-apply(simp add: flip_def fresh_def supp_swap)
-apply(rule alpha_weird_raw.intros)
-apply(simp add: alpha_weird_raw.intros(2))
-done*)
 
 text {* example 1 *}
 
@@ -245,8 +140,8 @@
   Vr2 "name"
 | Ap2 "trm2" "trm2"
 | Lm2 x::"name" t::"trm2"       bind x in t
-| Lt2 r::"rassign" t::"trm2"    bind "bv2 r" in t
-and rassign = 
+| Lt2 r::"assign" t::"trm2"    bind "bv2 r" in t
+and assign = 
   As "name" "trm2"
 binder
   bv2