--- a/doc-src/IsarRef/Thy/document/Proof.tex Thu May 15 20:02:42 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Thu May 15 20:02:44 2008 +0200
@@ -217,7 +217,7 @@
of the premises of the rule involved. Note that positions may be
easily skipped using something like \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}~\isa{{\isachardoublequote}{\isacharunderscore}\ {\isasymAND}\ a\ {\isasymAND}\ b{\isachardoublequote}}, for example. This involves the trivial rule
\isa{{\isachardoublequote}PROP\ {\isasympsi}\ {\isasymLongrightarrow}\ PROP\ {\isasympsi}{\isachardoublequote}}, which is bound in Isabelle/Pure as
- ``\indexref{}{fact}{\_}\hyperlink{fact.-}{\mbox{\isa{{\isacharunderscore}}}}'' (underscore).
+ ``\indexref{}{fact}{\_}\hyperlink{fact.underscore}{\mbox{\isa{{\isacharunderscore}}}}'' (underscore).
Automated methods (such as \hyperlink{method.simp}{\mbox{\isa{simp}}} or \hyperlink{method.auto}{\mbox{\isa{auto}}}) just
insert any given facts before their usual operation. Depending on
@@ -635,7 +635,7 @@
goal statements with a list of patterns ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}''. In both cases, higher-order matching is invoked to
bind extra-logical term variables, which may be either named
schematic variables of the form \isa{{\isacharquery}x}, or nameless dummies
- ``\hyperlink{variable.-}{\mbox{\isa{{\isacharunderscore}}}}'' (underscore). Note that in the \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}
+ ``\hyperlink{variable.underscore}{\mbox{\isa{{\isacharunderscore}}}}'' (underscore). Note that in the \hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}}
form the patterns occur on the left-hand side, while the \hyperlink{keyword.is}{\mbox{\isa{\isakeyword{is}}}} patterns are in postfix position.
Polymorphism of term bindings is handled in Hindley-Milner style,
--- a/doc-src/IsarRef/Thy/document/intro.tex Thu May 15 20:02:42 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/intro.tex Thu May 15 20:02:44 2008 +0200
@@ -250,13 +250,10 @@
\begin{isamarkuptext}%
Isabelle/Isar provides a simple document preparation system based on
existing {PDF-\LaTeX} technology, with full support of hyper-links
- (both local references and URLs), bookmarks, and thumbnails. Thus
- the results are equally well suited for WWW browsing and as printed
- copies.
+ (both local references and URLs) and bookmarks. Thus the results
+ are equally well suited for WWW browsing and as printed copies.
- \medskip
-
- Isabelle generates {\LaTeX} output as part of the run of a
+ \medskip Isabelle generates {\LaTeX} output as part of the run of a
\emph{logic session} (see also \cite{isabelle-sys}). Getting
started with a working configuration for common situations is quite
easy by using the Isabelle \verb|mkdir| and \verb|make|