# HG changeset patch
# User huffman
# Date 1228444666 28800
# Node ID 3d8f01383117ec532cb21d4322ec745bc1ef54bb
# Parent  a301dc6c6a37f710c806f285055c1adb6888fec8
fix proofs

diff -r a301dc6c6a37 -r 3d8f01383117 src/HOL/Tools/ComputeNumeral.thy
--- a/src/HOL/Tools/ComputeNumeral.thy	Thu Dec 04 16:44:37 2008 -0800
+++ b/src/HOL/Tools/ComputeNumeral.thy	Thu Dec 04 18:37:46 2008 -0800
@@ -116,7 +116,7 @@
 lemma nat_norm_number_of: "nat_norm_number_of (number_of w) = (if lezero w then 0 else number_of w)"
   apply (simp add: nat_norm_number_of_def)
   unfolding lezero_def iszero_def neg_def
-  apply (simp add: number_of_is_id)
+  apply (simp add: numeral_simps)
   done
 
 (* Normalization of nat literals *)
@@ -143,6 +143,7 @@
   apply (auto simp add: number_of_is_id neg_def iszero_def)
   apply (case_tac "x > 0")
   apply auto
+  apply (rule order_less_imp_le)
   apply (simp add: mult_strict_left_mono[where a=y and b=0 and c=x, simplified])
   done