*** empty log message ***
Fri, 19 Aug 2005 18:38:59 +0200
changeset 17127 65e340b6a56f
parent 17126 ff9ad5b17100
child 17128 bb09ba3e5b2f
*** empty log message ***
--- 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}!\\
-  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}.