--- a/src/HOL/Matrix/ComputeNumeral.thy Mon Mar 01 12:30:55 2010 +0100
+++ b/src/HOL/Matrix/ComputeNumeral.thy Mon Mar 01 13:42:31 2010 +0100
@@ -20,7 +20,7 @@
lemmas bitiszero = iszero1 iszero2 iszero3 iszero4
(* lezero for bit strings *)
-constdefs
+definition
"lezero x == (x \<le> 0)"
lemma lezero1: "lezero Int.Pls = True" unfolding Int.Pls_def lezero_def by auto
lemma lezero2: "lezero Int.Min = True" unfolding Int.Min_def lezero_def by auto
@@ -60,7 +60,7 @@
lemmas bitarith = bitnorm bitiszero bitneg bitlezero biteq bitless bitle bitsucc bitpred bituminus bitadd bitmul
-constdefs
+definition
"nat_norm_number_of (x::nat) == x"
lemma nat_norm_number_of: "nat_norm_number_of (number_of w) = (if lezero w then 0 else number_of w)"