--- a/src/HOL/IMP/Abs_Int3.thy Thu Feb 20 12:27:51 2014 +1100
+++ b/src/HOL/IMP/Abs_Int3.thy Wed Feb 19 22:05:05 2014 +0100
@@ -260,7 +260,7 @@
end
-interpretation Abs_Int_wn
+permanent_interpretation Abs_Int_wn
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -545,7 +545,7 @@
split: prod.splits if_splits extended.split)
-interpretation Abs_Int_wn_measure
+permanent_interpretation Abs_Int_wn_measure
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
and test_num' = in_ivl
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl