--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Wed Feb 19 22:05:05 2014 +0100
@@ -47,13 +47,13 @@
end
-interpretation Rep rep_cval
+permanent_interpretation Rep rep_cval
proof
case goal1 thus ?case
by(cases a, cases b, simp, simp, cases b, simp, simp)
qed
-interpretation Val_abs rep_cval Const plus_cval
+permanent_interpretation Val_abs rep_cval Const plus_cval
proof
case goal1 show ?case by simp
next
@@ -61,7 +61,7 @@
by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
qed
-interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
+permanent_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
defines AI_const is AI
and aval'_const is aval'
proof qed (auto simp: iter'_pfp_above)