--- a/src/HOL/Datatype.thy Fri Oct 20 10:44:36 2006 +0200
+++ b/src/HOL/Datatype.thy Fri Oct 20 10:44:37 2006 +0200
@@ -731,7 +731,7 @@
"is_none None = True"
"is_none (Some x) = False"
-lemma is_none_none [code inline]:
+lemma is_none_none [code inline, symmetric, normal post]:
"(x = None) = (is_none x)"
by (cases x) simp_all
--- a/src/HOL/Integ/IntArith.thy Fri Oct 20 10:44:36 2006 +0200
+++ b/src/HOL/Integ/IntArith.thy Fri Oct 20 10:44:37 2006 +0200
@@ -398,11 +398,11 @@
"number_of (k::int) = k"
unfolding int_number_of_def by simp
-lemma zero_is_num_zero [code inline]:
+lemma zero_is_num_zero [code inline, symmetric, normal post]:
"(0::int) = number_of Numeral.Pls"
by simp
-lemma one_is_num_one [code inline]:
+lemma one_is_num_one [code inline, symmetric, normal post]:
"(1::int) = number_of (Numeral.Pls BIT bit.B1)"
by simp