src/ZF/Integ/Int.ML
changeset 8201 a81d18b0a9b1
parent 6153 bff90585cce5
child 9333 5cacc383157a
     1.1 --- a/src/ZF/Integ/Int.ML	Sat Feb 05 17:31:53 2000 +0100
     1.2 +++ b/src/ZF/Integ/Int.ML	Mon Feb 07 15:14:02 2000 +0100
     1.3 @@ -193,7 +193,7 @@
     1.4  by (rtac bexI 1);
     1.5  by (rtac (add_diff_inverse2 RS sym) 1);
     1.6  by Auto_tac;
     1.7 -by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1);
     1.8 +by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le]) 1);
     1.9  qed "not_zneg_int_of";
    1.10  
    1.11  Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z";