# HG changeset patch
# User nipkow
# Date 1365340114 -7200
# Node ID 6034362836867fec6fa845eda000e5c7a57b6fca
# Parent  f0b375b692927b4ef06b2396c78d217ef62b64b1
cleaned

diff -r f0b375b69292 -r 603436283686 src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Sun Apr 07 10:06:37 2013 +0200
+++ b/src/HOL/IMP/Collecting.thy	Sun Apr 07 15:08:34 2013 +0200
@@ -22,13 +22,6 @@
 "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