# HG changeset patch
# User nipkow
# Date 971762434 -7200
# Node ID 692e29b9d2b292786560c26903b5742deb2d8dca
# Parent  2c0ad01ddaf74fb169c3ad2bd7000d9b89fca184
<= -> \<le>

diff -r 2c0ad01ddaf7 -r 692e29b9d2b2 src/HOL/Ord.thy
--- a/src/HOL/Ord.thy	Mon Oct 16 20:33:15 2000 +0200
+++ b/src/HOL/Ord.thy	Tue Oct 17 08:00:34 2000 +0200
@@ -61,8 +61,8 @@
 syntax (symbols)
   "_lessAll" :: [idt, 'a, bool] => bool   ("(3\\<forall>_<_./ _)"  [0, 0, 10] 10)
   "_lessEx"  :: [idt, 'a, bool] => bool   ("(3\\<exists>_<_./ _)"  [0, 0, 10] 10)
-  "_leAll"   :: [idt, 'a, bool] => bool   ("(3\\<forall>_<=_./ _)" [0, 0, 10] 10)
-  "_leEx"    :: [idt, 'a, bool] => bool   ("(3\\<exists>_<=_./ _)" [0, 0, 10] 10)
+  "_leAll"   :: [idt, 'a, bool] => bool   ("(3\\<forall>_\\<le>_./ _)" [0, 0, 10] 10)
+  "_leEx"    :: [idt, 'a, bool] => bool   ("(3\\<exists>_\\<le>_./ _)" [0, 0, 10] 10)
 
 syntax (HOL)
   "_lessAll" :: [idt, 'a, bool] => bool   ("(3! _<_./ _)"  [0, 0, 10] 10)