src/HOL/IMP/Collecting.thy

 "Step f g S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
   IF b THEN {g b S} Step f g P1 C1 ELSE {g (Not b) S} Step f g P2 C2
   {post C1 \<squnion> post C2}" |
 "Step f g S ({I} WHILE b DO {P} C {Q}) =
   {S \<squnion> post C} WHILE b DO {g b I} Step f g P C {g (Not b) I}"
-
-(* Could hide f and g like this:
-consts fa :: "vname \<Rightarrow> aexp \<Rightarrow> 'a \<Rightarrow> 'a::sup"
-       fb :: "bexp \<Rightarrow> 'a \<Rightarrow> 'a::sup"
-abbreviation "STEP == Step fa fb"
-thm Step.simps[where f = fa and g = fb]
-*)
 
 lemma strip_Step[simp]: "strip(Step f g S C) = strip C"
 by(induct C arbitrary: S) auto