diff -r 1810b1ade437 -r 47ee18b6ae32 src/HOL/Matrix/ComputeNumeral.thy
--- 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)"