--- a/Nominal-General/Nominal2_Base.thy	Fri Oct 01 07:11:47 2010 -0400
+++ b/Nominal-General/Nominal2_Base.thy	Mon Oct 04 07:25:37 2010 +0100
@@ -1247,6 +1247,10 @@
 where 
   "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x"
 
+lemma fresh_star_supp_conv:
+  shows "supp x \<sharp>* y \<Longrightarrow> supp y \<sharp>* x"
+by (auto simp add: fresh_star_def fresh_def)
+
 lemma fresh_star_prod:
   fixes as::"atom set"
   shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 
@@ -1482,9 +1486,8 @@
 apply(simp add: supp_Pair)
 apply(rule_tac x="p" in exI)
 apply(simp add: fresh_star_prod)
-apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")
-apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]
-apply(auto simp add: fresh_star_def fresh_def)
+apply(rule fresh_star_supp_conv)
+apply(auto simp add: fresh_star_def)
 done
 
 lemma at_set_avoiding2_atom:

--- a/Nominal/Ex/Let.thy	Fri Oct 01 07:11:47 2010 -0400
+++ b/Nominal/Ex/Let.thy	Mon Oct 04 07:25:37 2010 +0100
@@ -97,15 +97,19 @@
 apply(simp add: finite_supp)
 apply(simp add: finite_supp)
 apply(simp add: trm_assn.fresh fresh_star_def)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs, fv_bn assn) \<and> supp ([bn assn]lst.trm) \<sharp>* q")
+apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs) \<and> supp ([bn assn]lst.trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
+apply(subgoal_tac "-q \<bullet> (\<forall>assn trm. (set (bn assn) \<sharp>* c \<and>  y = Let assn trm) \<longrightarrow> P)")
+apply(perm_simp add: trm_assn.fv_bn_eqvt)
+(* HERE *)
+
+
+
 apply(simp add: set_eqvt)
 apply(subst (asm) tt)
 apply(rule_tac assms(4))
 apply(simp add: fresh_star_prod)
-apply(erule conjE)
-apply(assumption)
 apply(simp)
 apply(simp add: trm_assn.eq_iff)
 apply(drule supp_perm_eq[symmetric])

--- a/Paper/Paper.thy	Fri Oct 01 07:11:47 2010 -0400
+++ b/Paper/Paper.thy	Mon Oct 04 07:25:37 2010 +0100
@@ -546,10 +546,10 @@
   such approximations can be simplified with the notion \emph{supports}, defined 
   as follows:
 
-  \begin{defn}
+  \begin{definition}
   A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
   not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
-  \end{defn}
+  \end{definition}
 
   \noindent
   The main point of @{text supports} is that we can establish the following 
@@ -779,7 +779,7 @@
   \emph{abstractions}. The important property we need to derive is the support of 
   abstractions, namely:
 
-  \begin{thm}[Support of Abstractions]\label{suppabs} 
+  \begin{theorem}[Support of Abstractions]\label{suppabs} 
   Assuming @{text x} has finite support, then\\[-6mm] 
   \begin{center}
   \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
@@ -788,7 +788,7 @@
   @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]}
   \end{tabular}
   \end{center}
-  \end{thm}
+  \end{theorem}
 
   \noindent
   Below we will show the first equation. The others 
@@ -2088,7 +2088,7 @@
   Two formalisations involving general binders have been 
   performed in older
   versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W 
-  \cite{BengtsonParow09, UrbanNipkow09}).  Both
+  \cite{BengtsonParow09,UrbanNipkow09}).  Both
   use the approach based on iterated single binders. Our experience with
   the latter formalisation has been disappointing. The major pain arose from
   the need to ``unbind'' variables. This can be done in one step with our

--- a/Paper/document/root.tex	Fri Oct 01 07:11:47 2010 -0400
+++ b/Paper/document/root.tex	Mon Oct 04 07:25:37 2010 +0100
@@ -1,9 +1,9 @@
-\documentclass{sigplanconf}
+\documentclass{llncs}
 \usepackage{isabelle}
 \usepackage{isabellesym}
 \usepackage{amsmath}
 \usepackage{amssymb}
-\usepackage{amsthm}
+%%\usepackage{amsthm}
 \usepackage{tikz}
 \usepackage{pgf}
 \usepackage{pdfsetup}
@@ -47,12 +47,12 @@
 
 \newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
 %----------------- theorem definitions ----------
-\theoremstyle{plain}
-\newtheorem{thm}{Theorem}[section]
-\newtheorem{property}[thm]{Property}
-\newtheorem{lemma}[thm]{Lemma}
-\newtheorem{defn}[thm]{Definition}
-\newtheorem{exmple}[thm]{Example}
+%%\theoremstyle{plain}
+%%\spnewtheorem{thm}[section]{Theorem}
+%%\newtheorem{property}[thm]{Property}
+%%\newtheorem{lemma}[thm]{Lemma}
+%%\spnewtheorem{defn}[theorem]{Definition}
+%%\spnewtheorem{exmple}[theorem]{Example}
 
 %-------------------- environment definitions -----------------
 \newenvironment{proof-of}[1]{{\em Proof of #1:}}{}
@@ -60,10 +60,10 @@
 
 \begin{document}
 
-\title{\LARGE\bf General Bindings and Alpha-Equivalence in Nominal Isabelle}
-\authorinfo{Christian Urban and Cezary Kaliszyk}
-           {TU Munich, Germany}
-           {\{urbanc, kaliszyk\}@in.tum.de}
+\title{General Bindings and Alpha-Equivalence in Nominal Isabelle}
+\author{Christian Urban and Cezary Kaliszyk}
+\institute{TU Munich, Germany}
+%%%{\{urbanc, kaliszyk\}@in.tum.de}
 \maketitle
 
 \begin{abstract} 
@@ -84,11 +84,11 @@
 
 %\category{F.4.1}{subcategory}{third-level}
 
-\terms
-formal reasoning, programming language calculi
+%\terms
+%formal reasoning, programming language calculi
 
-\keywords
-nominal logic work, variable convention
+%\keywords
+%nominal logic work, variable convention
 
 
 \input{session}