src/HOL/Integ/NatBin.thy
changeset 13491 ddf6ae639f21
parent 13189 81ed5c6de890
child 14194 8953b566dfed
     1.1 --- a/src/HOL/Integ/NatBin.thy	Mon Aug 12 17:48:15 2002 +0200
     1.2 +++ b/src/HOL/Integ/NatBin.thy	Mon Aug 12 17:48:19 2002 +0200
     1.3 @@ -26,10 +26,10 @@
     1.4  declare split_div[of _ _ "number_of k", standard, arith_split]
     1.5  declare split_mod[of _ _ "number_of k", standard, arith_split]
     1.6  
     1.7 -lemma nat_number_of_Pls: "number_of Pls = (0::nat)"
     1.8 +lemma nat_number_of_Pls: "number_of bin.Pls = (0::nat)"
     1.9    by (simp add: number_of_Pls nat_number_of_def)
    1.10  
    1.11 -lemma nat_number_of_Min: "number_of Min = (0::nat)"
    1.12 +lemma nat_number_of_Min: "number_of bin.Min = (0::nat)"
    1.13    apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
    1.14    apply (simp add: neg_nat)
    1.15    done