diff -r 589daaf48dba -r 0a6d576da295 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Fri Apr 05 20:54:55 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Sat Apr 06 18:42:55 2013 +0200
@@ -25,10 +25,10 @@
 
 definition less_option where "x < (y::'a option) = (x \<le> y \<and> \<not> y \<le> x)"
 
-lemma [simp]: "(x \<le> None) = (x = None)"
+lemma le_None[simp]: "(x \<le> None) = (x = None)"
 by (cases x) simp_all
 
-lemma [simp]: "(Some x \<le> u) = (\<exists>y. u = Some y \<and> x \<le> y)"
+lemma Some_le[simp]: "(Some x \<le> u) = (\<exists>y. u = Some y \<and> x \<le> y)"
 by (cases u) auto
 
 instance proof