src/HOL/IMP/Abs_Int0_const.thy
changeset 45655 a49f9428aba4
parent 45623 f682f3f7b726
child 46039 698de142f6f9
--- a/src/HOL/IMP/Abs_Int0_const.thy	Sat Nov 26 17:10:03 2011 +0100
+++ b/src/HOL/IMP/Abs_Int0_const.thy	Sun Nov 27 13:31:52 2011 +0100
@@ -68,7 +68,7 @@
 
 interpretation Abs_Int rep_cval Const plus_cval
 defines AI_const is AI
-and step_const is step
+and step_const is step'
 proof qed