# HG changeset patch
# User huffman
# Date 1228527322 28800
# Node ID a47003001699208d3596fbc330dcc898caf76b59
# Parent  5cd646abf6bcda691f266129e6e67984fb2024ab
simplify less_nat_number_of

diff -r 5cd646abf6bc -r a47003001699 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Fri Dec 05 17:26:16 2008 -0800
+++ b/src/HOL/NatBin.thy	Fri Dec 05 17:35:22 2008 -0800
@@ -258,12 +258,10 @@
 
 subsubsection{*Less-than (<) *}
 
-(*"neg" is used in rewrite rules for binary comparisons*)
 lemma less_nat_number_of [simp]:
-     "((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))"
-  unfolding neg_def nat_number_of_def number_of_is_id
+  "(number_of v :: nat) < number_of v' \<longleftrightarrow>
+    (if v < v' then Int.Pls < v' else False)"
+  unfolding nat_number_of_def number_of_is_id numeral_simps
   by auto