src/HOL/Ord.thy
changeset 10227 692e29b9d2b2
parent 8882 9df44a4f1bf7
child 10427 9d2de9b6e7f4
--- 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)