
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/SubstAx.thy
--- 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}"
 




