--- 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