src/HOL/IMP/AbsInt2.thy

 proof qed
   (auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
 
 end
 
-instantiation astate :: (WN)WN
+instantiation astate :: (WN) WN
 begin
 
 definition "widen_astate F1 F2 =
   FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
 

     by(auto simp: narrow_astate_def le_astate_def lookup_def narrow2)
 qed
 
 end
 
-instantiation up :: (WN)WN
+instantiation up :: (WN) WN
 begin
 
 fun widen_up where
 "widen_up bot x = x" |
 "widen_up x bot = x" |

 qed
 
 end
 
 interpretation
-  Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter' 3 2)"
+  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
 defines afilter_ivl' is afilter
 and bfilter_ivl' is bfilter
 and AI_ivl' is AI
 and aval_ivl' is aval'
 proof qed (auto simp: iter'_pfp_above)