src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy

     by (blast intro: mono_gamma_c order_trans)
 qed
 
 end
 
-permanent_interpretation Abs_Int2
+global_interpretation Abs_Int2
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 defines AI_ivl' = AI_wn
 ..