# HG changeset patch
# User wenzelm
# Date 1555256225 -7200
# Node ID 48e8bbeef7d3235f54bec9595d51596457c29314
# Parent  1f163f772da30eabf89b288fdda46f59a82a1e45
obsolete -- this is quite fast;

diff -r 1f163f772da3 -r 48e8bbeef7d3 src/HOL/ex/PresburgerEx.thy
--- 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