obsolete (see f3378101f555);
authorwenzelm
Fri, 05 Mar 2021 22:23:57 +0100
changeset 73391 f16f209f996c
parent 73390 3c5a7746ffa4
child 73392 24f0df084aad
obsolete (see f3378101f555);
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))