--- a/src/ZF/UNITY/ClientImpl.thy Sat Nov 01 11:40:55 2014 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy Sat Nov 01 14:20:38 2014 +0100
@@ -105,14 +105,14 @@
lemma preserves_lift_imp_stable:
- "G \<in> preserves(lift(ff)) ==> G \<in> stable({s \<in> state. P(s`ff)})";
+ "G \<in> preserves(lift(ff)) ==> G \<in> stable({s \<in> state. P(s`ff)})"
apply (drule preserves_imp_stable)
apply (simp add: lift_def)
done
lemma preserves_imp_prefix:
"G \<in> preserves(lift(ff))
- ==> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})";
+ ==> G \<in> stable({s \<in> state. \<langle>k, s`ff\<rangle> \<in> prefix(nat)})"
by (erule preserves_lift_imp_stable)
(*Safety property 1 \<in> ask, rel are increasing: (24) *)