--- a/doc-src/IsarRef/isar-ref.tex Thu May 08 22:48:09 2008 +0200
+++ b/doc-src/IsarRef/isar-ref.tex Thu May 08 22:48:33 2008 +0200
@@ -55,20 +55,6 @@
\chardef\charbackquote=`\`
\newcommand{\backquote}{\mbox{\tt\charbackquote}}
-\newcommand{\drv}{\mathrel{\vdash}}
-\newcommand{\edrv}{\mathop{\drv}\nolimits}
-\newcommand{\Or}{\mathrel{\;|\;}}
-
-\renewcommand{\vec}[1]{\overline{#1}}
-
-\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
-
-\pagestyle{headings}
-\sloppy
-\binperiod %%%treat . like a binary operator
-
-\renewcommand{\phi}{\varphi}
-
\begin{document}