| changeset 61671 | 20d4cd2ceab2 |
| parent 58310 | 91ea607a34d8 |
| child 61890 | f6ded81f5690 |
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Sat Nov 14 08:45:52 2015 +0100 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Sat Nov 14 08:45:52 2015 +0100 @@ -62,7 +62,7 @@ qed permanent_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)" -defining AI_const = AI +defines AI_const = AI and aval'_const = aval' proof qed (auto simp: iter'_pfp_above)