--- a/src/HOL/SMT_Examples/SMT_Examples.thy Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy Mon Nov 24 12:35:13 2014 +0100
@@ -354,9 +354,6 @@
lemma "\<exists>x::int. \<forall>x y. 0 < x \<and> 0 < y \<longrightarrow> (0::int) < x + y" by smt
lemma "\<exists>u::int. \<forall>(x::int) y::real. 0 < x \<and> 0 < y \<longrightarrow> -1 < x" by smt
lemma "\<exists>x::int. (\<forall>y. y \<ge> x \<longrightarrow> y > 0) \<longrightarrow> x > 0" by smt
-lemma "\<forall>x::int.
- SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat x) SMT.Symb_Nil) SMT.Symb_Nil)
- (x < a \<longrightarrow> 2 * x < 2 * a)" by smt
lemma "\<forall>(a::int) b::int. 0 < b \<or> b < 1" by smt