# HG changeset patch
# User wenzelm
# Date 1614979437 -3600
# Node ID f16f209f996c9d49fb719430503ec56bff716f19
# Parent  3c5a7746ffa4b22590b1cd221c55c77e6f1ef6d2
obsolete (see f3378101f555);

diff -r 3c5a7746ffa4 -r f16f209f996c src/HOL/SMT_Examples/SMT_Examples_Verit.thy
--- a/src/HOL/SMT_Examples/SMT_Examples_Verit.thy	Fri Mar 05 21:26:38 2021 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples_Verit.thy	Fri Mar 05 22:23:57 2021 +0100
@@ -314,7 +314,6 @@
          x6 = \<bar>x5\<bar> - x4; x7 = \<bar>x6\<bar> - x5; x8 = \<bar>x7\<bar> - x6;
          x9 = \<bar>x8\<bar> - x7; x10 = \<bar>x9\<bar> - x8; x11 = \<bar>x10\<bar> - x9 \<rbrakk>
  \<Longrightarrow> x1 = x10 \<and> x2 = (x11::int)"
-  supply [[smt_timeout=360]]
   by (smt (verit))