fixed typos
authorkleing
Mon, 06 Dec 2004 01:06:22 +0100 (2004-12-06)
changeset 15373 cf912e83bf6f
parent 15372 2ecc0befd98f
child 15374 3849153b850e
fixed typos
doc-src/LaTeXsugar/Sugar/Sugar.thy
--- 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},