# HG changeset patch # User Christian Urban # Date 1288970470 0 # Node ID 8cf5c3e58889096d9e95a1911f65b5044c9302e4 # Parent 2668486b684a4d590a8fc581ebef5debbc44be2c small typo diff -r 2668486b684a -r 8cf5c3e58889 Paper/Paper.thy --- a/Paper/Paper.thy Fri Oct 29 15:37:24 2010 +0100 +++ b/Paper/Paper.thy Fri Nov 05 15:21:10 2010 +0000 @@ -524,11 +524,11 @@ swapping two fresh atoms, say @{text a} and @{text b}, leaves @{text x} unchanged, namely if @{text "a \ x"} and @{text "b \ x"} then @{term "(a \ b) \ x"}. - + % %\begin{myproperty}\label{swapfreshfresh} %@{thm[mode=IfThen] swap_fresh_fresh[no_vars]} %\end{myproperty} - + % %While often the support of an object can be relatively easily %described, for example for atoms, products, lists, function applications, %booleans and permutations as follows @@ -553,7 +553,7 @@ %\noindent %in some cases it can be difficult to characterise the support precisely, and %only an approximation can be established (as for functions above). - + % %Reasoning about %such approximations can be simplified with the notion \emph{supports}, defined %as follows: @@ -603,7 +603,7 @@ %Using freshness, the nominal logic work provides us with general means for renaming %binders. % - \noindent + %\noindent While in the older version of Nominal Isabelle, we used extensively %Property~\ref{swapfreshfresh} this property to rename single binders, it %%this property