--- a/src/HOL/IMP/Collecting.thy Sun Jan 01 09:27:48 2012 +0100
+++ b/src/HOL/IMP/Collecting.thy Sun Jan 01 16:32:53 2012 +0100
@@ -171,7 +171,7 @@
{S \<union> post c} WHILE b DO (step {s:Inv. bval b s} c) {{s:Inv. \<not> bval b s}}"
definition CS :: "state set \<Rightarrow> com \<Rightarrow> state set acom" where
-"CS S c = lfp c (step S)"
+"CS S c = lfp (step S) c"
lemma mono_step_aux: "x \<le> y \<Longrightarrow> S \<subseteq> T \<Longrightarrow> step S x \<le> step T y"
proof(induction x y arbitrary: S T rule: less_eq_acom.induct)
@@ -190,7 +190,7 @@
lemma strip_step: "strip(step S c) = strip c"
by (induction c arbitrary: S) auto
-lemma lfp_cs_unfold: "lfp c (step S) = step S (lfp c (step S))"
+lemma lfp_cs_unfold: "lfp (step S) c = step S (lfp (step S) c)"
apply(rule lfp_unfold[OF _ mono_step])
apply(simp add: strip_step)
done