# HG changeset patch
# User huffman
# Date 1329996274 -3600
# Node ID c71f3e9367bb0c0fa2946a55065c69b6843aed8f
# Parent  be67deaea7608050840e229f8b8dd5d18175c617
remove unnecessary lemmas

diff -r be67deaea760 -r c71f3e9367bb src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Feb 23 12:08:59 2012 +0100
+++ b/src/HOL/Word/Word.thy	Thu Feb 23 12:24:34 2012 +0100
@@ -790,14 +790,6 @@
   shows "bl_to_bin (bin_to_bl (len_of TYPE('a)) (uint x)) = uint x"
   by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])
 
-(* FIXME: the next two lemmas should be unnecessary, because the lhs
-terms should never occur in practice *)
-lemma num_AB_u [simp]: "number_of (uint x) = x"
-  unfolding word_number_of_def by (rule word_uint.Rep_inverse)
-
-lemma num_AB_s [simp]: "number_of (sint x) = x"
-  unfolding word_number_of_def by (rule word_sint.Rep_inverse)
-
 (* naturals *)
 lemma uints_unats: "uints n = int ` unats n"
   apply (unfold unats_def uints_num)