# HG changeset patch
# User nipkow
# Date 1124469539 -7200
# Node ID 65e340b6a56f36a11379dc77cb2aa50ab0bcd0e7
# Parent  ff9ad5b17100ea804e3d27862f9098dd9dc02b14
*** empty log message ***

diff -r ff9ad5b17100 -r 65e340b6a56f doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Aug 19 11:03:06 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Aug 19 18:38:59 2005 +0200
@@ -128,7 +128,7 @@
 
 (*<*)ML"reset show_question_marks"(*>*)
 
-subsection "Variable names"
+subsection {*Variable names\label{sec:varnames}*}
 
 text{* It sometimes happens that you want to change the name of a
 variable in a theorem before printing it. This can easily be achieved
@@ -249,15 +249,9 @@
 subsection "Patterns"
 
 text {*
-  Sometimes functions ignore one or more of their
-  arguments and some functional languages have nice 
-  syntax for that as in @{thm hd.simps [where xs=DUMMY]}.
 
-  You can simulate this in Isabelle by instantiating the @{term xs} in
-  definition \mbox{@{thm hd.simps}} with a constant @{text DUMMY} that
-  is printed as @{term DUMMY}. The code for the pattern above is 
-  \verb!@!\verb!{thm hd.simps [where xs=DUMMY]}!.
-
+  In \S\ref{sec:varnames} we shows how to create patterns containing
+  ``@{term DUMMY}''.
   You can drive this game even further and extend the syntax of let
   bindings such that certain functions like @{term fst}, @{term hd}, 
   etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
@@ -380,8 +374,7 @@
     \verb!@!\verb!{thm_style [show_types] concl hd_Cons_tl}!\\
     \verb!\end{center}!
   \end{quote}
-
-  Be aware that any options must be placed \emph{before}
+  Beware that any options must be placed \emph{before}
   the name of the style, as in this example.
 
   Further use cases can be found in \S\ref{sec:yourself}.