src/HOL/IMP/Abs_Int2_ivl.thy

 lemma add_mono_Fin_le:
   "\<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
 
 global_interpretation Val_semilattice
-where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "(+)"
 proof (standard, goal_cases)
   case 1 thus ?case by transfer (simp add: le_iff_subset)
 next
   case 2 show ?case by transfer (simp add: \<gamma>_rep_def)
 next

     by(auto simp: empty_rep_def is_empty_rep_def)
 qed
 
 
 global_interpretation Val_lattice_gamma
-where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "(+)"
 defines aval_ivl = aval'
 proof (standard, goal_cases)
   case 1 show ?case by(simp add: \<gamma>_inf)
 next
   case 2 show ?case unfolding bot_ivl_def by transfer simp
 qed
 
 global_interpretation Val_inv
-where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "(+)"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
 proof (standard, goal_cases)
   case 1 thus ?case by transfer (auto simp: \<gamma>_rep_def)
 next

     apply(simp add: \<gamma>_aboveI[of i2] \<gamma>_belowI[of i1])
     done
 qed
 
 global_interpretation Abs_Int_inv
-where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "(+)"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
 defines inv_aval_ivl = inv_aval'
 and inv_bval_ivl = inv_bval'
 and step_ivl = step'

 apply transfer
 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)
 
 global_interpretation Abs_Int_inv_mono
-where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
+where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "(+)"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
 proof (standard, goal_cases)
   case 1 thus ?case by (rule mono_plus_ivl)
 next