# HG changeset patch # User Cezary Kaliszyk # Date 1315975224 -32400 # Node ID e57c175d9214c8b42c2bc5f19576ffa590318088 # Parent 01a3861035d46ee6ea300a759ca2203af780bd1a minor diff -r 01a3861035d4 -r e57c175d9214 LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Tue Sep 13 19:48:47 2011 +0200 +++ b/LMCS-Paper/Paper.thy Wed Sep 14 13:40:24 2011 +0900 @@ -1294,8 +1294,8 @@ \emph{free-atom functions} from the specifications.\footnote{Admittedly, the details of our definitions will be somewhat involved. However they are still conceptually simple in comparison with the ``positional'' approach taken in - Ott \cite[Pages 88--95]{ott-jfp}, which uses the notions of \emph{occurences} and - \emph{partial equivalence relations} over sets of occurences.} For the + Ott \cite[Pages 88--95]{ott-jfp}, which uses the notions of \emph{occurrences} and + \emph{partial equivalence relations} over sets of occurrences.} For the \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions \begin{equation}\label{fvars} diff -r 01a3861035d4 -r e57c175d9214 LMCS-Paper/document/root.tex --- a/LMCS-Paper/document/root.tex Tue Sep 13 19:48:47 2011 +0200 +++ b/LMCS-Paper/document/root.tex Wed Sep 14 13:40:24 2011 +0900 @@ -72,7 +72,7 @@ \author{Cezary Kaliszyk} \address{University of Tsukuba, Japan} -\email{kaliszyk@score.cs.tsukuba.ac.jp} +\email{kaliszyk@cs.tsukuba.ac.jp} \thanks{$^\star$~This is a revised and expanded version of~\cite{UrbanKaliszyk11}} \keywords{Nominal Isabelle, variable convention, theorem provers, formal reasoning,lambda-calculus}