# HG changeset patch
# User paulson
# Date 957458457 -7200
# Node ID 4a3612f30865071d47465f56c845230c7e96c188
# Parent  3b10d24b5eddfa13404ddae42310788577c98f88
if_weak_cong should make linear arithmetic faster

diff -r 3b10d24b5edd -r 4a3612f30865 src/HOL/Integ/IntArith.ML
--- 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