--- a/src/HOL/Real/HahnBanach/document/notation.tex Fri Jul 07 16:48:12 2000 +0200
+++ b/src/HOL/Real/HahnBanach/document/notation.tex Fri Jul 07 17:15:17 2000 +0200
@@ -10,6 +10,8 @@
\newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
+\newcommand{\skp}{\smallskip}
+
\newcommand{\To}{\to}
\newcommand{\dt}{{\mathpunct.}}
\newcommand{\Ex}[1]{\exists #1\dt\;}
@@ -19,7 +21,7 @@
\newcommand{\Impl}{\Rightarrow}
\newcommand{\And}{\;\land\;}
\newcommand{\Or}{\;\lor\;}
-\newcommand{\Le}{\le}
+\newcommand{\Le}{\leq}
\newcommand{\Lt}{\lt}
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
\newcommand{\ap}{\mathpalette{\mathbin{\!}}{\mathbin{\!}}{\mathbin{}}{\mathbin{}}}