| changeset 55600 | 3c7610b8dcfc |
| parent 55599 | 6535c537b243 |
| child 56927 | 4044a7d1720f |
--- a/src/HOL/IMP/Abs_Int1_parity.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int1_parity.thy Wed Feb 19 22:05:15 2014 +0100 @@ -125,7 +125,7 @@ permanent_interpretation Abs_Int where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity -defines aval_parity is aval' and step_parity is step' and AI_parity is AI +defining aval_parity = aval' and step_parity = step' and AI_parity = AI ..