--- a/src/HOL/IMP/Abs_Int1.thy Fri Jan 27 14:30:44 2012 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy Fri Jan 27 17:02:08 2012 +0100
@@ -61,7 +61,7 @@
end
locale Val_abs1_gamma =
- Val_abs where \<gamma> = \<gamma> for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set" +
+ Gamma where \<gamma> = \<gamma> for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set" +
assumes inter_gamma_subset_gamma_meet:
"\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"
and gamma_Bot[simp]: "\<gamma> \<bottom> = {}"