| changeset 16184 | 80617b8d33c5 |
| parent 15097 | b807858b97bd |
| child 16417 | 9bc16273c2d4 |
--- a/src/HOL/UNITY/Simple/Reach.thy Thu Jun 02 13:17:06 2005 +0200 +++ b/src/HOL/UNITY/Simple/Reach.thy Thu Jun 02 13:47:08 2005 +0200 @@ -62,7 +62,7 @@ lemma reach_invariant: "Rprg \<in> Always reach_invariant" apply (rule AlwaysI, force) -apply (unfold Rprg_def, constrains) +apply (unfold Rprg_def, safety) apply (blast intro: rtrancl_trans) done