| changeset 55600 | 3c7610b8dcfc |
| parent 55599 | 6535c537b243 |
| child 58249 | 180f1b3508ed |
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Wed Feb 19 22:05:05 2014 +0100 +++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy Wed Feb 19 22:05:15 2014 +0100 @@ -115,7 +115,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 ..