# HG changeset patch
# User haftmann
# Date 1161333877 -7200
# Node ID bc1fa6f47ced22ffaa07d31cd09997264483c9c9
# Parent  361e62500ab74576393a2cfede11c292d3b2e869
added normal post setup

diff -r 361e62500ab7 -r bc1fa6f47ced src/HOL/Datatype.thy
--- 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
 
diff -r 361e62500ab7 -r bc1fa6f47ced src/HOL/Integ/IntArith.thy
--- 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