--- a/src/HOL/IMP/Abs_Int0.thy Tue Jul 02 20:47:32 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Wed Jul 03 16:07:00 2013 +0200
@@ -148,7 +148,7 @@
text{* The interface for abstract values: *}
-locale Val_abs =
+locale Val_semilattice =
fixes \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
assumes mono_gamma: "a \<le> b \<Longrightarrow> \<gamma> a \<le> \<gamma> b"
and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
@@ -163,7 +163,7 @@
the name of the type parameter @{typ 'av} which would otherwise be renamed to
@{typ 'a}. *}
-locale Abs_Int_fun = Val_abs where \<gamma>=\<gamma>
+locale Abs_Int_fun = Val_semilattice where \<gamma>=\<gamma>
for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
begin