src/HOL/UNITY/Constrains.thy
changeset 6823 97babc436a41
parent 6705 b2662096ccd0
child 13797 baefae13ad37
     1.1 --- a/src/HOL/UNITY/Constrains.thy	Sun Jun 13 13:52:50 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Constrains.thy	Sun Jun 13 13:53:33 1999 +0200
     1.3 @@ -32,7 +32,8 @@
     1.4  	   ==> s' : reachable F"
     1.5  
     1.6  consts
     1.7 -  Co, Unless :: "['a set, 'a set] => 'a program set"       (infixl 60)
     1.8 +  Constrains :: "['a set, 'a set] => 'a program set"  (infixl "Co"     60)
     1.9 +  op_Unless  :: "['a set, 'a set] => 'a program set"  (infixl "Unless" 60)
    1.10  
    1.11  defs
    1.12    Constrains_def