# HG changeset patch
# User wenzelm
# Date 1210279713 -7200
# Node ID b54a1a7856646856d924679ec54d3faf1cc98e27
# Parent  c7709b3e1a4eba672a83694e5911b1b2a5e28cfa
removed obsolete math macros;

diff -r c7709b3e1a4e -r b54a1a785664 doc-src/IsarRef/isar-ref.tex
--- 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}