src/HOL/SMT_Examples/SMT_Examples.thy

 lemma "(p \<and> True) = p" by smt
 
 lemma "(p \<or> q) \<and> \<not>p \<Longrightarrow> q" by smt
 
 lemma "(a \<and> b) \<or> (c \<and> d) \<Longrightarrow> (a \<and> b) \<or> (c \<and> d)"
-  using [[smt_oracle=true]] (* no Z3 proof *)
   by smt
 
 lemma "(p1 \<and> p2) \<or> p3 \<longrightarrow> (p1 \<longrightarrow> (p3 \<and> p2) \<or> (p1 \<and> p3)) \<or> p1" by smt
 
 lemma "P=P=P=P=P=P=P=P=P=P" by smt

 
 
 subsection {* Non-linear arithmetic over integers and reals *}
 
 lemma "a > (0::int) \<Longrightarrow> a*b > 0 \<Longrightarrow> b > 0"
-  using [[smt_oracle=true]]  -- {* Isabelle's arithmetic decision procedures
-    are too weak to automatically prove @{thm zero_less_mult_pos}. *}
-  by smt (* FIXME: use z3_rule *)
-
-
-
-lemma  "(a::int) * (x + 1 + y) = a * x + a * (y + 1)" by smt
-
-lemma "((x::real) * (1 + y) - x * (1 - y)) = (2 * x * y)" by smt
+  using zero_less_mult_pos
+  by smt
+
+lemma  "(a::int) * (x + 1 + y) = a * x + a * (y + 1)"
+  using right_distrib
+  by smt
+
+lemma "((x::real) * (1 + y) - x * (1 - y)) = (2 * x * y)"
+  sorry (* FIXME: Z3 could solve this directly *)
 
 lemma
   "(U::int) + (1 + p) * (b + e) + p * d =
    U + (2 * (1 + p) * (b + e) + (1 + p) * d + d * p) - (1 + p) * (b + d + e)"
-  by smt
+  sorry (* FIXME: Z3 could solve this directly *)
 
 
 subsection {* Linear arithmetic for natural numbers *}
 
 lemma "2 * (x::nat) ~= 1" by smt