src/HOL/UNITY/ListOrder.thy
changeset 80914 d97fdabd9e2b
parent 67613 ce654b0e6d69
--- a/src/HOL/UNITY/ListOrder.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/UNITY/ListOrder.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -49,11 +49,11 @@
     "Ge == {(x,y). y <= x}"
 
 abbreviation
-  pfixLe :: "[nat list, nat list] => bool"  (infixl "pfixLe" 50)  where
+  pfixLe :: "[nat list, nat list] => bool"  (infixl \<open>pfixLe\<close> 50)  where
   "xs pfixLe ys == (xs,ys) \<in> genPrefix Le"
 
 abbreviation
-  pfixGe :: "[nat list, nat list] => bool"  (infixl "pfixGe" 50)  where
+  pfixGe :: "[nat list, nat list] => bool"  (infixl \<open>pfixGe\<close> 50)  where
   "xs pfixGe ys == (xs,ys) \<in> genPrefix Ge"