| changeset 17668 | 8ef257366a0c |
| parent 17550 | 9bcd6ea262b8 |
| child 17724 | e969fc0a4925 |
--- a/src/HOL/Integ/NatBin.thy Tue Sep 27 12:14:39 2005 +0200 +++ b/src/HOL/Integ/NatBin.thy Tue Sep 27 12:16:06 2005 +0200 @@ -28,8 +28,6 @@ lemma nat_number_of [simp]: "nat (number_of w) = number_of w" by (simp add: nat_number_of_def) -declare nat_number_of [symmetric, THEN eq_reflection, code unfold] - lemma nat_numeral_0_eq_0 [simp]: "Numeral0 = (0::nat)" by (simp add: nat_number_of_def)