# HG changeset patch
# User wenzelm
# Date 1210874564 -7200
# Node ID 0265353e4def4e415fb047d5e704b81790e76937
# Parent  871cc7f11034c8cf4a71e334df0893d195114dde
updated generated file;

diff -r 871cc7f11034 -r 0265353e4def doc-src/IsarRef/Thy/document/Proof.tex
--- 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,
diff -r 871cc7f11034 -r 0265353e4def doc-src/IsarRef/Thy/document/intro.tex
--- 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|