author | wenzelm |
Fri, 05 Mar 2021 22:23:57 +0100 | |
changeset 73391 | f16f209f996c |
parent 73390 | 3c5a7746ffa4 |
child 73392 | 24f0df084aad |
--- 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))