# HG changeset patch
# User huffman
# Date 1228526776 28800
# Node ID 5cd646abf6bcda691f266129e6e67984fb2024ab
# Parent  49f602ae24e5bd2a0218bab22245321804c17f71
add lemma le_nat_number_of

diff -r 49f602ae24e5 -r 5cd646abf6bc src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Fri Dec 05 11:42:27 2008 +0100
+++ b/src/HOL/NatBin.thy	Fri Dec 05 17:26:16 2008 -0800
@@ -267,6 +267,14 @@
   by auto
 
 
+subsubsection{*Less-than-or-equal *}
+
+lemma le_nat_number_of [simp]:
+  "(number_of v :: nat) \<le> number_of v' \<longleftrightarrow>
+    (if v \<le> v' then True else v \<le> Int.Pls)"
+  unfolding nat_number_of_def number_of_is_id numeral_simps
+  by auto
+
 (*Maps #n to n for n = 0, 1, 2*)
 lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2