| changeset 16417 | 9bc16273c2d4 |
| parent 14150 | 9a23e4eb5eb3 |
| child 19769 | c40ce2de2020 |
--- a/src/HOL/UNITY/SubstAx.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/UNITY/SubstAx.thy Fri Jun 17 16:12:49 2005 +0200 @@ -8,7 +8,7 @@ header{*Weak Progress*} -theory SubstAx = WFair + Constrains: +theory SubstAx imports WFair Constrains begin constdefs Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60)