some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x;
removed historic note about Poly/ML vs. SML/NJ;
--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy Sat Apr 28 11:24:20 2012 +0200
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Sat Apr 28 16:06:30 2012 +0200
@@ -168,12 +168,11 @@
Common mathematical symbols such as @{text \<forall>} are represented in
Isabelle as @{verbatim \<forall>}. There are infinitely many Isabelle
symbols like this, although proper presentation is left to front-end
- tools such as {\LaTeX} or Proof~General with the X-Symbol package.
- A list of predefined Isabelle symbols that work well with these
- tools is given in \appref{app:symbols}. Note that @{verbatim "\<lambda>"}
- does not belong to the @{text letter} category, since it is already
- used differently in the Pure term language.
-*}
+ tools such as {\LaTeX}, Proof~General, or Isabelle/jEdit. A list of
+ predefined Isabelle symbols that work well with these tools is given
+ in \appref{app:symbols}. Note that @{verbatim "\<lambda>"} does not belong
+ to the @{text letter} category, since it is already used differently
+ in the Pure term language. *}
section {* Common syntax entities *}
--- a/doc-src/IsarRef/Thy/Symbols.thy Sat Apr 28 11:24:20 2012 +0200
+++ b/doc-src/IsarRef/Thy/Symbols.thy Sat Apr 28 16:06:30 2012 +0200
@@ -14,8 +14,7 @@
appropriate definitions of @{verbatim "\\"}@{verbatim isasym}@{text
name} for each @{verbatim "\\"}@{verbatim "<"}@{text name}@{verbatim
">"} in the @{verbatim isabellesym.sty} file. Most of these symbols
- are displayed properly in Proof~General if used with the X-Symbol
- package.
+ are displayed properly in Proof~General and Isabelle/jEdit.
Moreover, any single symbol (or ASCII character) may be prefixed by
@{verbatim "\\"}@{verbatim "<^sup>"}, for superscript and @{verbatim
--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Sat Apr 28 11:24:20 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Sat Apr 28 16:06:30 2012 +0200
@@ -183,11 +183,11 @@
Common mathematical symbols such as \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}} are represented in
Isabelle as \verb|\<forall>|. There are infinitely many Isabelle
symbols like this, although proper presentation is left to front-end
- tools such as {\LaTeX} or Proof~General with the X-Symbol package.
- A list of predefined Isabelle symbols that work well with these
- tools is given in \appref{app:symbols}. Note that \verb|\<lambda>|
- does not belong to the \isa{letter} category, since it is already
- used differently in the Pure term language.%
+ tools such as {\LaTeX}, Proof~General, or Isabelle/jEdit. A list of
+ predefined Isabelle symbols that work well with these tools is given
+ in \appref{app:symbols}. Note that \verb|\<lambda>| does not belong
+ to the \isa{letter} category, since it is already used differently
+ in the Pure term language.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/IsarRef/Thy/document/Symbols.tex Sat Apr 28 11:24:20 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Symbols.tex Sat Apr 28 16:06:30 2012 +0200
@@ -29,8 +29,7 @@
The collection of predefined standard symbols given below is
available by default for Isabelle document output, due to
appropriate definitions of \verb|\|\verb|isasym|\isa{name} for each \verb|\|\verb|<|\isa{name}\verb|>| in the \verb|isabellesym.sty| file. Most of these symbols
- are displayed properly in Proof~General if used with the X-Symbol
- package.
+ are displayed properly in Proof~General and Isabelle/jEdit.
Moreover, any single symbol (or ASCII character) may be prefixed by
\verb|\|\verb|<^sup>|, for superscript and \verb|\|\verb|<^sub>|, for subscript, such as \verb|A\|\verb|<^sup>\<star>|, for \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{5C3C737461723E}{\isasymstar}}{\isaliteral{22}{\isachardoublequote}}} the alternative
--- a/doc-src/System/Thy/Interfaces.thy Sat Apr 28 11:24:20 2012 +0200
+++ b/doc-src/System/Thy/Interfaces.thy Sat Apr 28 16:06:30 2012 +0200
@@ -62,12 +62,13 @@
interface} script.
\item[@{setting_def XSYMBOL_INSTALLFONTS}] may contain a small shell
- script to install the X11 fonts required for the X-Symbols mode of
- Proof General. This is only relevant if the X11 display server runs
- on a different machine than the Emacs application, with a different
- file-system view on the Proof General installation. Under most
- circumstances Proof General is able to refer to the font files that
- are part of its distribution.
+ script to install the X11 fonts required for the old X-Symbols mode
+ of Proof General. This is only relevant if the X11 display server
+ runs on a different machine than the Emacs application, with a
+ different file-system view on the Proof General installation. Under
+ most circumstances Proof General 3.x is able to refer to the font
+ files that are part of its distribution, and Proof General 4.x finds
+ its fonts by different means.
\end{description}
*}
--- a/doc-src/System/Thy/document/Interfaces.tex Sat Apr 28 11:24:20 2012 +0200
+++ b/doc-src/System/Thy/document/Interfaces.tex Sat Apr 28 16:06:30 2012 +0200
@@ -82,12 +82,13 @@
the command line of any invocation of the Proof General \verb|interface| script.
\item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isaliteral{5F}{\isacharunderscore}}INSTALLFONTS}}}}}] may contain a small shell
- script to install the X11 fonts required for the X-Symbols mode of
- Proof General. This is only relevant if the X11 display server runs
- on a different machine than the Emacs application, with a different
- file-system view on the Proof General installation. Under most
- circumstances Proof General is able to refer to the font files that
- are part of its distribution.
+ script to install the X11 fonts required for the old X-Symbols mode
+ of Proof General. This is only relevant if the X11 display server
+ runs on a different machine than the Emacs application, with a
+ different file-system view on the Proof General installation. Under
+ most circumstances Proof General 3.x is able to refer to the font
+ files that are part of its distribution, and Proof General 4.x finds
+ its fonts by different means.
\end{description}%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Documents/Documents.thy Sat Apr 28 11:24:20 2012 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy Sat Apr 28 16:06:30 2012 +0200
@@ -148,10 +148,10 @@
(*>*)
text {*
- \noindent The X-Symbol package within Proof~General provides several
- input methods to enter @{text \<oplus>} in the text. If all fails one may
- just type a named entity \verb,\,\verb,<oplus>, by hand; the
- corresponding symbol will be displayed after further input.
+ \noindent Proof~General provides several input methods to enter
+ @{text \<oplus>} in the text. If all fails one may just type a named
+ entity \verb,\,\verb,<oplus>, by hand; the corresponding symbol will
+ be displayed after further input.
More flexible is to provide alternative syntax forms
through the \bfindex{print mode} concept~\cite{isabelle-ref}. By
--- a/doc-src/TutorialI/Documents/document/Documents.tex Sat Apr 28 11:24:20 2012 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Sat Apr 28 16:06:30 2012 +0200
@@ -182,10 +182,10 @@
\endisadelimML
%
\begin{isamarkuptext}%
-\noindent The X-Symbol package within Proof~General provides several
- input methods to enter \isa{{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}} in the text. If all fails one may
- just type a named entity \verb,\,\verb,<oplus>, by hand; the
- corresponding symbol will be displayed after further input.
+\noindent Proof~General provides several input methods to enter
+ \isa{{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}} in the text. If all fails one may just type a named
+ entity \verb,\,\verb,<oplus>, by hand; the corresponding symbol will
+ be displayed after further input.
More flexible is to provide alternative syntax forms
through the \bfindex{print mode} concept~\cite{isabelle-ref}. By
--- a/doc-src/TutorialI/preface.tex Sat Apr 28 11:24:20 2012 +0200
+++ b/doc-src/TutorialI/preface.tex Sat Apr 28 16:06:30 2012 +0200
@@ -35,17 +35,11 @@
from output generated in this way. The final chapter of Part~I explains how
users may produce their own formal documents in a similar fashion.
-Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains links to
-the download area and to documentation and other information. Most Isabelle
-sessions are now run from within David Aspinall's\index{Aspinall, David}
-wonderful user interface, \hfootref{http://proofgeneral.inf.ed.ac.uk/}{Proof
- General}, even together with the
-\hfootref{http://x-symbol.sourceforge.net}{X-Symbol} package for XEmacs. This
-book says very little about Proof General, which has its own documentation.
-In order to run Isabelle, you will need a Standard ML compiler. We recommend
-\hfootref{http://www.polyml.org/}{Poly/ML}, which is free and gives the best
-performance. The other fully supported compiler is
-\hfootref{http://www.smlnj.org/index.html}{Standard ML of New Jersey}.
+Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains
+links to the download area and to documentation and other information.
+The classic Isabelle user interface is Proof~General~/ Emacs by David
+Aspinall's\index{Aspinall, David}. This book says very little about
+Proof General, which has its own documentation.
This tutorial owes a lot to the constant discussions with and the valuable
feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf