src/HOL/Integ/int_arith1.ML
changeset 14378 69c4d5997669
parent 14369 c50188fe6366
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -28,6 +28,11 @@
     1.4  val bin_mult_Min = thm"bin_mult_Min";
     1.5  val bin_mult_BIT = thm"bin_mult_BIT";
     1.6  
     1.7 +val neg_def = thm "neg_def";
     1.8 +val iszero_def = thm "iszero_def";
     1.9 +val not_neg_int = thm "not_neg_int";
    1.10 +val neg_zminus_int = thm "neg_zminus_int";
    1.11 +
    1.12  val zadd_ac = thms "Ring_and_Field.add_ac"
    1.13  val zmult_ac = thms "Ring_and_Field.mult_ac"
    1.14  val NCons_Pls_0 = thm"NCons_Pls_0";