changeset 15373 cf912e83bf6f
parent 15368 79f624f97f7f
child 15378 b1c5add0a65e
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Mon Dec 06 01:05:58 2004 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Mon Dec 06 01:06:22 2004 +0100
@@ -245,7 +245,7 @@
   You can simulate this in Isabelle by instantiating the @{term xs} in
   definition \mbox{@{thm hd.simps[no_vars]}} 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,novars]}!.
+  \verb!@!\verb!{thm hd.simps [where xs=DUMMY,no_vars]}!.
   You can drive this game even further and extend the syntax of let
   bindings such that certain functions like @{term fst}, @{term hd},