src/ZF/UNITY/ClientImpl.thy
changeset 58860 fee7cfa69c50
parent 46953 2b6e55924af3
child 61392 331be2820f90
     1.1 --- a/src/ZF/UNITY/ClientImpl.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/ZF/UNITY/ClientImpl.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -105,14 +105,14 @@
     1.4  
     1.5  
     1.6  lemma preserves_lift_imp_stable:
     1.7 -     "G \<in> preserves(lift(ff)) ==> G \<in> stable({s \<in> state. P(s`ff)})";
     1.8 +     "G \<in> preserves(lift(ff)) ==> G \<in> stable({s \<in> state. P(s`ff)})"
     1.9  apply (drule preserves_imp_stable)
    1.10  apply (simp add: lift_def)
    1.11  done
    1.12  
    1.13  lemma preserves_imp_prefix:
    1.14       "G \<in> preserves(lift(ff))
    1.15 -      ==> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})";
    1.16 +      ==> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})"
    1.17  by (erule preserves_lift_imp_stable)
    1.18  
    1.19  (*Safety property 1 \<in> ask, rel are increasing: (24) *)