
diff -r 8932f33259d4 -r 97babc436a41 src/HOL/UNITY/Constrains.thy
--- a/src/HOL/UNITY/Constrains.thy	Sun Jun 13 13:52:50 1999 +0200
+++ b/src/HOL/UNITY/Constrains.thy	Sun Jun 13 13:53:33 1999 +0200
@@ -32,7 +32,8 @@
 	   ==> s' : reachable F"
 
 consts
-  Co, Unless :: "['a set, 'a set] => 'a program set"       (infixl 60)
+  Constrains :: "['a set, 'a set] => 'a program set"  (infixl "Co"     60)
+  op_Unless  :: "['a set, 'a set] => 'a program set"  (infixl "Unless" 60)
 
 defs
   Constrains_def




