| changeset 55600 | 3c7610b8dcfc |
| parent 55599 | 6535c537b243 |
| child 58249 | 180f1b3508ed |
--- a/src/HOL/IMP/Abs_Int1_const.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int1_const.thy Wed Feb 19 22:05:15 2014 +0100 @@ -69,7 +69,7 @@ permanent_interpretation Abs_Int where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const -defines AI_const is AI and step_const is step' and aval'_const is aval' +defining AI_const = AI and step_const = step' and aval'_const = aval' ..