--- a/src/HOL/IMP/Abs_Int2_ivl.thy Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy Sat Dec 19 11:05:04 2015 +0100
@@ -302,7 +302,7 @@
"\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2"
by(drule (1) add_mono) simp
-permanent_interpretation Val_semilattice
+global_interpretation Val_semilattice
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
proof (standard, goal_cases)
case 1 thus ?case by transfer (simp add: le_iff_subset)
@@ -318,7 +318,7 @@
qed
-permanent_interpretation Val_lattice_gamma
+global_interpretation Val_lattice_gamma
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
defines aval_ivl = aval'
proof (standard, goal_cases)
@@ -327,7 +327,7 @@
case 2 show ?case unfolding bot_ivl_def by transfer simp
qed
-permanent_interpretation Val_inv
+global_interpretation Val_inv
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
@@ -350,7 +350,7 @@
done
qed
-permanent_interpretation Abs_Int_inv
+global_interpretation Abs_Int_inv
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
@@ -384,7 +384,7 @@
apply(auto simp: below_rep_def le_iff_subset split: if_splits prod.split)
by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
-permanent_interpretation Abs_Int_inv_mono
+global_interpretation Abs_Int_inv_mono
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