# HG changeset patch
# User wenzelm
# Date 1509199949 -7200
# Node ID d4f7c6f14fa2ba12edebe2b8af98b8e1ef4dbd38
# Parent  c19b17b7277737cc7190293cb9a82156ebf8d8f9
avoid slow proofs due to simp rules from 960509bfd47e;

diff -r c19b17b72777 -r d4f7c6f14fa2 src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Fri Oct 27 17:06:30 2017 +0200
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Oct 28 16:12:29 2017 +0200
@@ -330,7 +330,7 @@
   from this[OF x_lower x_upper x_lower' x_upper' \<open>0 <= 0\<close> \<open>0 <= 79\<close>]
     \<open>0 \<le> ca\<close> \<open>0 \<le> ce\<close> x_lower x_lower'
   show ?thesis unfolding returns(1) returns(2) unfolding returns
-    by simp
+    by (simp del: mod_pos_pos_trivial mod_neg_neg_trivial)
 qed
 
 spark_vc procedure_round_62
@@ -415,7 +415,8 @@
     \<open>0 \<le> cla\<close> \<open>0 \<le> cle\<close> \<open>0 \<le> cra\<close> \<open>0 \<le> cre\<close> x_lower x_lower'
   show ?thesis unfolding \<open>loop__1__j + 1 + 1 = loop__1__j + 2\<close>
     unfolding returns(1) returns(2) unfolding returns
-    by simp
+    by (simp del: mod_pos_pos_trivial mod_neg_neg_trivial)
+
 qed
 
 spark_vc procedure_round_76