src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy

--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy	Fri Dec 18 14:23:11 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy	Sat Dec 19 11:05:04 2015 +0100
@@ -52,7 +52,7 @@
 end
 
 
-permanent_interpretation Val_abs
+global_interpretation Val_abs
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 proof
   case goal1 thus ?case
@@ -66,7 +66,7 @@
     by(auto simp: plus_const_cases split: const.split)
 qed
 
-permanent_interpretation Abs_Int
+global_interpretation Abs_Int
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 defines AI_const = AI and step_const = step' and aval'_const = aval'
 ..
@@ -114,7 +114,7 @@
 
 text{* Monotonicity: *}
 
-permanent_interpretation Abs_Int_mono
+global_interpretation Abs_Int_mono
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 proof
   case goal1 thus ?case