<= -> \<le>
authornipkow
Tue, 17 Oct 2000 08:00:34 +0200
changeset 10227 692e29b9d2b2
parent 10226 2c0ad01ddaf7
child 10228 e653cb933293
<= -> \<le>
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)