1.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Jul 18 13:49:26 2011 +0200
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Mon Jul 18 18:52:52 2011 +0200
     1.3 @@ -414,6 +414,15 @@
     1.4     U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)"
     1.5    by smt
     1.6  
     1.7 +lemma [z3_rule]:
     1.8 +  fixes x :: "int"
     1.9 +  assumes "x * y \<le> 0" and "\<not> y \<le> 0" and "\<not> x \<le> 0"
    1.10 +  shows False
    1.11 +  using assms by (metis mult_le_0_iff)
    1.12 +
    1.13 +lemma "x * y \<le> (0 :: int) \<Longrightarrow> x \<le> 0 \<or> y \<le> 0" by smt
    1.14 +
    1.15 +
    1.16  
    1.17  subsection {* Linear arithmetic for natural numbers *}
    1.18