src/HOL/Integ/NatBin.thy
changeset 11468 02cd5d5bc497
parent 11464 ddea204de5bc
child 12440 fb5851b71a82
     1.1 --- a/src/HOL/Integ/NatBin.thy	Mon Aug 06 16:43:40 2001 +0200
     1.2 +++ b/src/HOL/Integ/NatBin.thy	Tue Aug 07 16:36:52 2001 +0200
     1.3 @@ -18,10 +18,6 @@
     1.4      "number_of v == nat (number_of v)"
     1.5       (*::bin=>nat        ::bin=>int*)
     1.6  
     1.7 -axioms
     1.8 -neg_number_of_bin_pred_iff_0:
     1.9 -  "neg (number_of (bin_pred v)) = (number_of v = (0::nat))"
    1.10 -
    1.11  use "nat_bin.ML"	setup nat_bin_arith_setup
    1.12  
    1.13  end