# HG changeset patch
# User bauerg
# Date 962982917 -7200
# Node ID 0b8e87bb91d98946ecb534ca5ee5f0c52c83d194
# Parent  a0a7c31cdc398a2dcfe155fdabb3d8c2ac517627
skp; le;

diff -r a0a7c31cdc39 -r 0b8e87bb91d9 src/HOL/Real/HahnBanach/document/notation.tex
--- 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{}}}