--- a/src/HOL/Integ/Int_lemmas.ML Thu Feb 27 18:21:42 2003 +0100
+++ b/src/HOL/Integ/Int_lemmas.ML Thu Feb 27 18:22:49 2003 +0100
@@ -319,7 +319,7 @@
qed "zle_iff_zadd";
Goal "abs (int m) = int m";
-by (simp_tac (simpset() addsimps [zabs_def]) 1);
+by (simp_tac (simpset() addsimps [Int.zabs_def]) 1);
qed "abs_int_eq";
Addsimps [abs_int_eq];
@@ -394,7 +394,6 @@
by (auto_tac (claset(), simpset() addsimps [lemma, linorder_not_less]));
qed "zless_nat_conj";
-
(* a case theorem distinguishing non-negative and negative int *)
val prems = Goal