1.1 --- a/src/HOL/Word/Bit_Representation.thy	Tue Dec 27 12:37:11 2011 +0100
     1.2 +++ b/src/HOL/Word/Bit_Representation.thy	Tue Dec 27 12:49:03 2011 +0100
     1.3 @@ -561,11 +561,6 @@
     1.4  lemmas bintrunc_Min_minus_I = bmsts(2)
     1.5  lemmas bintrunc_BIT_minus_I = bmsts(3)
     1.6  
     1.7 -lemma bintrunc_0_Min: "bintrunc 0 Int.Min = Int.Pls"
     1.8 -  by (fact bintrunc.Z) (* FIXME: delete *)
     1.9 -lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Int.Pls"
    1.10 -  by (fact bintrunc.Z) (* FIXME: delete *)
    1.11 -
    1.12  lemma bintrunc_Suc_lem:
    1.13    "bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y"
    1.14    by auto