--- a/src/HOL/Integ/IntArith.ML Thu May 04 18:39:51 2000 +0200
+++ b/src/HOL/Integ/IntArith.ML Thu May 04 18:40:57 2000 +0200
@@ -415,7 +415,8 @@
LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [add1_zle_eq RS iffD2];
LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
- addsimprocs simprocs;
+ addsimprocs simprocs
+ addcongs [if_weak_cong];
LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("IntDef.int",true)]
end;
@@ -546,6 +547,10 @@
by Auto_tac;
qed "nat_eq_iff";
+Goal "#0 <= w ==> (m = nat w) = (w = int m)";
+by Auto_tac;
+qed "nat_eq_iff2";
+
Goal "#0 <= w ==> (nat w < m) = (w < int m)";
by (rtac iffI 1);
by (asm_full_simp_tac