nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:26d594a9b89f
+:bf4b28ebb412
 text {*
 \noindent
 The code of the quotient package and the examples described here are already
 included in the standard distribution of Isabelle.
-%  \footnote{Available from \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.}
+\footnote{Available from \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.}
 The package is
 heavily used in the new version of Nominal Isabelle, which provides a
 convenient reasoning infrastructure for programming language calculi
 involving general binders.  To achieve this, it builds types representing
 @{text \<alpha>}-equivalent terms.  Earlier versions of Nominal Isabelle have been
 %%
 %% give an example for this
 %%
 \medskip
-%  \noindent
+\noindent
-%  {\bf Acknowledgements:} We would like to thank Peter Homeier for the many
+{\bf Acknowledgements:} We would like to thank Peter Homeier for the many
-%  discussions about his HOL4 quotient package and explaining to us
+discussions about his HOL4 quotient package and explaining to us
-%  some of its finer points in the implementation. Without his patient
+some of its finer points in the implementation. Without his patient
-%  help, this work would have been impossible.
+help, this work would have been impossible.
 *}