src/HOL/IMP/Abs_Int1_const.thy

 qed
 
 end
 
 
-interpretation Val_semilattice
+permanent_interpretation Val_semilattice
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 proof
   case goal1 thus ?case
     by(cases a, cases b, simp, simp, cases b, simp, simp)
 next

 next
   case goal4 thus ?case
     by(auto simp: plus_const_cases split: const.split)
 qed
 
-interpretation Abs_Int
+permanent_interpretation Abs_Int
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 defines AI_const is AI and step_const is step' and aval'_const is aval'
 ..
 
 

 value "show_acom (the(AI_const test6_const))"
 
 
 text{* Monotonicity: *}
 
-interpretation Abs_Int_mono
+permanent_interpretation Abs_Int_mono
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 proof
   case goal1 thus ?case
     by(auto simp: plus_const_cases split: const.split)
 qed

 text{* Termination: *}
 
 definition m_const :: "const \<Rightarrow> nat" where
 "m_const x = (if x = Any then 0 else 1)"
 
-interpretation Abs_Int_measure
+permanent_interpretation Abs_Int_measure
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 and m = m_const and h = "1"
 proof
   case goal1 thus ?case by(auto simp: m_const_def split: const.splits)
 next