# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1316497490 -32400
# Node ID 10e476d6f4b80f2c3b1b10946f139c74ba70414c
# Parent  a5a6aebec1fb7527abd6d121deba99ac117ef858
minor

diff -r a5a6aebec1fb -r 10e476d6f4b8 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Mon Sep 19 21:52:59 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Tue Sep 20 14:44:50 2011 +0900
@@ -2414,7 +2414,7 @@
   Another technique for representing binding is higher-order abstract syntax
   (HOAS), which for example is implemented in the Twelf system \cite{pfenningsystem}. 
   This representation technique supports very elegantly many aspects of
-  \emph{single} binding, and impressive work by Lee et al ~\cite{LeeCraryHarper07} 
+  \emph{single} binding, and impressive work by Lee et al~\cite{LeeCraryHarper07} 
   has been done that uses HOAS for mechanising the metatheory of SML. We
   are, however, not aware how multiple binders of SML are represented in this
   work. Judging from the submitted Twelf-solution for the POPLmark challenge,
diff -r a5a6aebec1fb -r 10e476d6f4b8 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Mon Sep 19 21:52:59 2011 +0200
+++ b/Nominal/Nominal2_Abs.thy	Tue Sep 20 14:44:50 2011 +0900
@@ -509,16 +509,13 @@
     (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y) \<and> supp p \<subseteq> set bsl \<union> set csl)"
   by (lifting alphas_abs_stronger)
 
+lemma alpha_res_alpha_set:
+  "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)"
+  using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast
+
 lemma Abs_eq_res_set:
   "(([bs]res. x) = ([cs]res. y)) = (([(bs \<inter> supp x)]set. x) = ([(cs \<inter> supp y)]set. y))"
-  unfolding Abs_eq_iff
-  using alpha_abs_set_abs_res alpha_abs_res_abs_set
-  apply auto
-  apply (rule_tac x="p" in exI)
-  apply assumption
-  apply (rule_tac x="p" in exI)
-  apply assumption
-  done
+  unfolding Abs_eq_iff alpha_res_alpha_set by rule
 
 lemma Abs_eq_res_supp:
   assumes asm: "supp x \<subseteq> bs"