equal
deleted
inserted
replaced
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: |