--- a/src/HOL/UNITY/GenPrefix.thy Sun Jun 13 13:53:33 1999 +0200
+++ b/src/HOL/UNITY/GenPrefix.thy Sun Jun 13 13:54:34 1999 +0200
@@ -44,12 +44,12 @@
"Ge == {(x,y). y <= x}"
syntax
- pfixLe :: [nat list, nat list] => bool (infixl "pfix'_le" 50)
- pfixGe :: [nat list, nat list] => bool (infixl "pfix'_ge" 50)
+ pfixLe :: [nat list, nat list] => bool (infixl "pfixLe" 50)
+ pfixGe :: [nat list, nat list] => bool (infixl "pfixGe" 50)
translations
- "xs pfix_le ys" == "(xs,ys) : genPrefix Le"
+ "xs pfixLe ys" == "(xs,ys) : genPrefix Le"
- "xs pfix_ge ys" == "(xs,ys) : genPrefix Ge"
+ "xs pfixGe ys" == "(xs,ys) : genPrefix Ge"
end