added normal post setup
authorhaftmann
Fri, 20 Oct 2006 10:44:37 +0200
changeset 21060 bc1fa6f47ced
parent 21059 361e62500ab7
child 21061 580dfc999ef6
added normal post setup
src/HOL/Datatype.thy
src/HOL/Integ/IntArith.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
 
--- 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