# HG changeset patch
# User paulson
# Date 929274813 -7200
# Node ID 97babc436a411ca7aa56c87c9787e9e6ccd2faaa
# Parent  8932f33259d41a75fda17c750e7a7d2a2ffca926
new-style infix directives

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
diff -r 8932f33259d4 -r 97babc436a41 src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Sun Jun 13 13:52:50 1999 +0200
+++ b/src/HOL/UNITY/UNITY.thy	Sun Jun 13 13:53:33 1999 +0200
@@ -15,7 +15,8 @@
   'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
 
 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)
 
 constdefs
     mk_program :: "('a set * ('a * 'a)set set) => 'a program"