Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
obsolete -- this is quite fast;
authorwenzelm
Sun, 14 Apr 2019 17:37:05 +0200
changeset 70165 48e8bbeef7d3
parent 70164 1f163f772da3
child 70166 538919322852
obsolete -- this is quite fast;
src/HOL/ex/PresburgerEx.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/PresburgerEx.thy	Sun Apr 14 13:32:26 2019 +0100
+++ b/src/HOL/ex/PresburgerEx.thy	Sun Apr 14 17:37:05 2019 +0200
@@ -88,7 +88,6 @@
 theorem "~ (\<forall>j (i::int). j \<le> i --> (\<exists>x y. 0 \<le> x & 0 \<le> y & 3 * x + 5 * y = i))"
   by presburger
 
-text\<open>Slow: about 5 seconds on a 1.6GHz machine.\<close>
 theorem "(\<exists>m::nat. n = 2 * m) --> (n + 1) div 2 = n div 2"
   by presburger
isabelle