--- 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