| changeset 26784 | eee21d6d0a6b |
| parent 25870 | a6a21adf3b55 |
| child 26911 | 871cc7f11034 |
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex Mon May 05 15:23:59 2008 +0200 +++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Mon May 05 15:27:13 2008 +0200 @@ -31,7 +31,6 @@ \newcommand{\isasymASSUME}{\cmd{assume}} \newcommand{\isasymSHOW}{\cmd{show}} \newcommand{\isasymNOTE}{\cmd{note}} -\newcommand{\isasymIN}{\cmd{in}} \newcommand{\isasymEXPORTCODE}{\cmd{export\_code}} \newcommand{\isasymCODEDATATYPE}{\cmd{code\_datatype}} \newcommand{\isasymCODECONST}{\cmd{code\_const}}