diff -r 6a4203148945 -r ddbf185a3be0 doc-src/IsarAdvanced/Classes/classes.tex
--- a/doc-src/IsarAdvanced/Classes/classes.tex	Fri Feb 23 08:39:19 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/classes.tex	Fri Feb 23 08:39:20 2007 +0100
@@ -10,6 +10,10 @@
 \usepackage{style}
 \usepackage{Thy/document/pdfsetup}
 
+\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
+\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
+\renewcommand{\isasymotimes}{\isamath{\circ}}
+
 \newcommand{\cmd}[1]{\isacommand{#1}}
 
 \newcommand{\isasymINFIX}{\cmd{infix}}