doc-src/IsarAdvanced/Classes/classes.tex
changeset 26784 eee21d6d0a6b
parent 25871 45753d56d935
child 26911 871cc7f11034
--- 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}"{}}