--- a/src/HOL/IMP/Abs_Int1.thy Tue Jul 02 20:47:32 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Wed Jul 03 16:07:00 2013 +0200
@@ -8,7 +8,7 @@
text{* Abstract interpretation over type @{text st} instead of functions. *}
-context Gamma
+context Gamma_semilattice
begin
fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
@@ -32,7 +32,7 @@
end
-locale Abs_Int = Gamma where \<gamma>=\<gamma>
+locale Abs_Int = Gamma_semilattice where \<gamma>=\<gamma>
for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
begin