doc-src/LaTeXsugar/Sugar/Sugar.thy
changeset 15373 cf912e83bf6f
parent 15368 79f624f97f7f
child 15378 b1c5add0a65e
equal deleted inserted replaced
15372:2ecc0befd98f 15373:cf912e83bf6f
   243   syntax for that as in @{thm hd.simps [where xs=DUMMY,no_vars]}.
   243   syntax for that as in @{thm hd.simps [where xs=DUMMY,no_vars]}.
   244 
   244 
   245   You can simulate this in Isabelle by instantiating the @{term xs} in
   245   You can simulate this in Isabelle by instantiating the @{term xs} in
   246   definition \mbox{@{thm hd.simps[no_vars]}} with a constant @{text DUMMY} that
   246   definition \mbox{@{thm hd.simps[no_vars]}} with a constant @{text DUMMY} that
   247   is printed as @{term DUMMY}. The code for the pattern above is 
   247   is printed as @{term DUMMY}. The code for the pattern above is 
   248   \verb!@!\verb!{thm hd.simps [where xs=DUMMY,novars]}!.
   248   \verb!@!\verb!{thm hd.simps [where xs=DUMMY,no_vars]}!.
   249 
   249 
   250   You can drive this game even further and extend the syntax of let
   250   You can drive this game even further and extend the syntax of let
   251   bindings such that certain functions like @{term fst}, @{term hd}, 
   251   bindings such that certain functions like @{term fst}, @{term hd}, 
   252   etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
   252   etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
   253   following:
   253   following: