Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SMT_Examples/SMT_Examples_Verit.thy
changeset 73391 f16f209f996c
parent 72908 6a26a955308e
child 74403 dbd69d287ec6 
--- 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))
isabelle