# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1315760669 -3600
# Node ID 41c1e98c686f9e581bc65f3422b4b916e791b764
# Parent  21674aea64e001a3075732cce4af7c79bbc67145
more

diff -r 21674aea64e0 -r 41c1e98c686f LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Sun Sep 11 10:42:13 2011 +0100
+++ b/LMCS-Paper/Paper.thy	Sun Sep 11 18:04:29 2011 +0100
@@ -728,7 +728,7 @@
   define
   
   \[
-  @{text "fa(x) = {x}"}  \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) = fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
+  @{text "fa(x) \<equiv> {x}"}  \hspace{5mm} @{text "fa(T\<^isub>1 \<rightarrow> T\<^isub>2) \<equiv> fa(T\<^isub>1) \<union> fa(T\<^isub>2)"}
   \]\smallskip
 
   \noindent
@@ -752,7 +752,7 @@
   In the rest of this section we are going to show that the alpha-equivalences really 
   lead to abstractions where some atoms are bound (more precisely removed from the 
   support).  For this we are going to introduce 
-  three abstraction types that are quotients with respect to the relations
+  three abstraction types that are quotients of the relations
 
   \begin{equation}
   \begin{array}{r}
@@ -1051,7 +1051,8 @@
   In these specifications @{text "name"} refers to an atom type, and @{text
   "fset"} to the type of finite sets.  Note that for @{text Lam} it does not
   matter which binding mode we use. The reason is that we bind only a single
-  @{text name}. However, having \isacommand{binds (set)} or just \isacommand{binds}
+  @{text name}, in which case all three binding modes coincide. However, having 
+  \isacommand{binds (set)} or just \isacommand{binds}
   in the second case makes a difference to the semantics of the specification
   (which we will define in the next section).
 
@@ -1414,14 +1415,14 @@
   
   \[\mbox{
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
-  @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\
-  @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\smallskip\\
+  @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "\<equiv>"} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\
+  @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "\<equiv>"} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\smallskip\\
 
-  @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
-  @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\smallskip\\
+  @{text "fa\<^bsub>assn\<^esub> (ANil)"} & @{text "\<equiv>"} & @{term "{}"}\\
+  @{text "fa\<^bsub>assn\<^esub> (ACons a t as)"} & @{text "\<equiv>"} & @{text "(supp a) \<union> (fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>assn\<^esub> as)"}\smallskip\\
 
-  @{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "="} & @{term "{}"}\\
-  @{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"}
+  @{text "fa\<^bsub>bn\<^esub> (ANil)"} & @{text "\<equiv>"} & @{term "{}"}\\
+  @{text "fa\<^bsub>bn\<^esub> (ACons a t as)"} & @{text "\<equiv>"} & @{text "(fa\<^bsub>trm\<^esub> t) \<union> (fa\<^bsub>bn\<^esub> as)"}
   \end{tabular}}
   \]\smallskip