--- a/doc-src/IsarAdvanced/Classes/classes.tex Mon May 05 15:23:59 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/classes.tex Mon May 05 15:27:13 2008 +0200
@@ -37,7 +37,6 @@
\newcommand{\isasymASSUME}{\cmd{assume}}
\newcommand{\isasymSHOW}{\cmd{show}}
\newcommand{\isasymNOTE}{\cmd{note}}
-\newcommand{\isasymIN}{\cmd{in}}
\newcommand{\qt}[1]{``#1''}
\newcommand{\qtt}[1]{"{}{#1}"{}}
--- 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}}
--- a/doc-src/IsarAdvanced/Functions/functions.tex Mon May 05 15:23:59 2008 +0200
+++ b/doc-src/IsarAdvanced/Functions/functions.tex Mon May 05 15:27:13 2008 +0200
@@ -33,7 +33,6 @@
\newcommand{\isasymASSUME}{\cmd{assume}}
\newcommand{\isasymSHOW}{\cmd{show}}
\newcommand{\isasymNOTE}{\cmd{note}}
-\newcommand{\isasymIN}{\cmd{in}}
\newcommand{\isasymCODEGEN}{\cmd{code\_gen}}
\newcommand{\isasymPRINTCODETHMS}{\cmd{print\_codethms}}
\newcommand{\isasymFUN}{\cmd{fun}}