# HG changeset patch
# User nipkow
# Date 1367373417 -7200
# Node ID ed847ce0b70cf7d6a2a49e7767e28fa22ed75a05
# Parent  b7a0af870bfc0f555a33946757ae95a36b5172df
tuned

diff -r b7a0af870bfc -r ed847ce0b70c src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Tue Apr 30 21:30:36 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Wed May 01 03:56:57 2013 +0200
@@ -38,7 +38,7 @@
 lemma in_gamma_inf: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"
 by (metis IntI inter_gamma_subset_gamma_inf set_mp)
 
-lemma gamma_inf[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
+lemma gamma_inf: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
 by(rule equalityI[OF _ inter_gamma_subset_gamma_inf])
   (metis inf_le1 inf_le2 le_inf_iff mono_gamma)