diff -r 750b63fa4c4e -r 52cd8bebc3b6 src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Tue Jul 02 20:47:32 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Wed Jul 03 16:07:00 2013 +0200
@@ -28,7 +28,7 @@
 
 subclass (in bounded_lattice) semilattice_sup_top ..
 
-locale Val_abs1_gamma = Gamma where \<gamma> = \<gamma>
+locale Val_lattice_gamma = Gamma_semilattice where \<gamma> = \<gamma>
   for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
 assumes inter_gamma_subset_gamma_inf:
   "\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"
@@ -45,7 +45,7 @@
 end
 
 
-locale Val_abs1 = Val_abs1_gamma where \<gamma> = \<gamma>
+locale Val_inv = Val_lattice_gamma where \<gamma> = \<gamma>
    for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
 fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"
 and inv_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
@@ -57,7 +57,7 @@
   i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1 : \<gamma> a\<^isub>1' \<and> i2 : \<gamma> a\<^isub>2'"
 
 
-locale Abs_Int1 = Val_abs1 where \<gamma> = \<gamma>
+locale Abs_Int_inv = Val_inv where \<gamma> = \<gamma>
   for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set"
 begin
 
@@ -184,7 +184,7 @@
 
 subsubsection "Monotonicity"
 
-locale Abs_Int1_mono = Abs_Int1 +
+locale Abs_Int_inv_mono = Abs_Int_inv +
 assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
 and mono_inv_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> r \<le> r' \<Longrightarrow>
   inv_plus' r a1 a2 \<le> inv_plus' r' b1 b2"