changeset 10834 | a7897aebbffc |
parent 10797 | 028d22926a41 |
child 13797 | baefae13ad37 |
--- a/src/HOL/UNITY/UNITY.thy Tue Jan 09 15:29:17 2001 +0100 +++ b/src/HOL/UNITY/UNITY.thy Tue Jan 09 15:32:27 2001 +0100 @@ -51,7 +51,7 @@ defs - constrains_def "A co B == {F. ALL act: Acts F. act```A <= B}" + constrains_def "A co B == {F. ALL act: Acts F. act``A <= B}" unless_def "A unless B == (A-B) co (A Un B)"