# HG changeset patch
# User kleing
# Date 1102291582 -3600
# Node ID cf912e83bf6fa44cb8682302cceb6d16324797bf
# Parent  2ecc0befd98f1ce03c9908ee253dd0e9bd7f2a21
fixed typos

diff -r 2ecc0befd98f -r cf912e83bf6f 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},