# HG changeset patch
# User paulson
# Date 1060789482 -7200
# Node ID fac076f0c71cf4bcade50b7d81e1100eab4d6bd9
# Parent  6580d374a509c4de4854bca34618380fc3c04ffc
reformatting change and mention of Introduction to Isabelle

diff -r 6580d374a509 -r fac076f0c71c doc-src/Ref/ref.tex
--- a/doc-src/Ref/ref.tex	Wed Aug 13 17:44:01 2003 +0200
+++ b/doc-src/Ref/ref.tex	Wed Aug 13 17:44:42 2003 +0200
@@ -12,18 +12,7 @@
 \author{{\em Lawrence C. Paulson}\\
         Computer Laboratory \\ University of Cambridge \\
         \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
-        With Contributions by Tobias Nipkow and Markus Wenzel%
-\thanks{Tobias Nipkow, of T. U. Munich, wrote most of
-  Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification},
-  and part of
-  Chapter~\protect\ref{theories}.  Carsten Clasohm also contributed to
-  Chapter~\protect\ref{theories}.  Markus Wenzel contributed to
-  Chapter~\protect\ref{chap:syntax}.  Jeremy Dawson, Sara Kalvala, Martin
-  Simons  and others suggested changes
-  and corrections.  The research has been funded by the EPSRC (grants
-  GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
-  (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
-  Schwerpunktprogramm \emph{Deduktion}.}}  
+        With Contributions by Tobias Nipkow and Markus Wenzel}  
 
 \makeindex
 
@@ -45,6 +34,31 @@
 \index{meta-rules|see{meta-rules}}
 
 \maketitle 
+\emph{Note}: this document is part of the earlier Isabelle documentation, 
+which is somewhat superseded by the Isabelle/HOL
+\emph{Tutorial}~\cite{isa-tutorial}. Much of it is concerned with 
+the old-style theory syntax and the primitives for conducting proofs 
+using the ML top level. This style of interaction is largely obsolete:
+most Isabelle proofs are now written using the Isar 
+language and the Proof General interface. However, this is the only
+comprehensive Isabelle reference manual.  
+
+See also the \emph{Introduction to Isabelle}, which has tutorial examples
+on conducting proofs using the ML top-level.
+
+\subsubsection*{Acknowledgements} 
+Tobias Nipkow, of T. U. Munich, wrote most of
+  Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification},
+  and part of
+  Chapter~\protect\ref{theories}.  Carsten Clasohm also contributed to
+  Chapter~\protect\ref{theories}.  Markus Wenzel contributed to
+  Chapter~\protect\ref{chap:syntax}.  Jeremy Dawson, Sara Kalvala, Martin
+  Simons  and others suggested changes
+  and corrections.  The research has been funded by the EPSRC (grants
+  GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
+  (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
+  Schwerpunktprogramm \emph{Deduktion}.
+
 \pagenumbering{roman} \tableofcontents \clearfirst
 
 \include{introduction}