| changeset 16184 | 80617b8d33c5 |
| parent 14094 | 33147ecac5f9 |
| child 16417 | 9bc16273c2d4 |
--- a/src/HOL/UNITY/Comp/Counterc.thy Thu Jun 02 13:17:06 2005 +0200 +++ b/src/HOL/UNITY/Comp/Counterc.thy Thu Jun 02 13:47:08 2005 +0200 @@ -87,7 +87,7 @@ lemma p2: "Component i \<in> stable {s. C s = (c s) i + k}" -by (simp add: Component_def, constrains) +by (simp add: Component_def, safety) lemma p3: "[| OK I Component; i\<in>I |]