| changeset 22347 | ddbf185a3be0 |
| parent 22317 | b550d2c6ca90 |
| child 23956 | 48494ccfabaf |
--- 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}}