| changeset 8122 | b43ad07660b9 |
| parent 8041 | e3237d8c18d6 |
| child 9685 | 6d123a7e30bd |
--- a/src/HOL/UNITY/SubstAx.thy Thu Jan 13 17:29:04 2000 +0100 +++ b/src/HOL/UNITY/SubstAx.thy Thu Jan 13 17:30:23 2000 +0100 @@ -9,6 +9,9 @@ SubstAx = WFair + Constrains + constdefs + Ensures :: "['a set, 'a set] => 'a program set" (infixl 60) + "A Ensures B == {F. F : (reachable F Int A) ensures B}" + LeadsTo :: "['a set, 'a set] => 'a program set" (infixl 60) "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"