src/HOL/IMP/Abs_Int1_ivl.thy

--- a/src/HOL/IMP/Abs_Int1_ivl.thy	Sat Nov 26 17:10:03 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Sun Nov 27 13:31:52 2011 +0100
@@ -207,7 +207,7 @@
   Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
 defines afilter_ivl is afilter
 and bfilter_ivl is bfilter
-and step_ivl is step
+and step_ivl is step'
 and AI_ivl is AI
 and aval_ivl' is aval''
 proof qed