# HG changeset patch
# User huffman
# Date 1228364657 28800
# Node ID 9f33ab8e15db6c4483aee673c3dd418751ea3ece
# Parent  011a6c86ab31675792b65b6e15c2a8ac56dc139e
simplify proof of less_nat_number_of

diff -r 011a6c86ab31 -r 9f33ab8e15db src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Wed Dec 03 15:04:37 2008 -0800
+++ b/src/HOL/NatBin.thy	Wed Dec 03 20:24:17 2008 -0800
@@ -264,9 +264,8 @@
      "((number_of v :: nat) < number_of v') =  
          (if neg (number_of v :: int) then neg (number_of (uminus v') :: int)  
           else neg (number_of (v + uminus v') :: int))"
-by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
-                nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
-         cong add: imp_cong, simp add: Pls_def)
+  unfolding neg_def nat_number_of_def number_of_is_id
+  by auto
 
 
 (*Maps #n to n for n = 0, 1, 2*)