diff -r 73e738371c90 -r 3e9e8dfb3c98 src/HOL/SMT_Examples/SMT_Examples.thy
--- a/src/HOL/SMT_Examples/SMT_Examples.thy	Thu May 27 14:54:13 2010 +0200
+++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Thu May 27 14:55:53 2010 +0200
@@ -335,11 +335,9 @@
 
 lemma "let P = 2 * x + 1 > x + (x::real) in P \<or> False \<or> P" by smt
 
-lemma "x + (let y = x mod 2 in 2 * y + 1) \<ge> x + (1::int)"
-  sorry (* FIXME: div/mod *)
+lemma "x + (let y = x mod 2 in 2 * y + 1) \<ge> x + (1::int)" by smt
 
-lemma "x + (let y = x mod 2 in y + y) < x + (3::int)"
-  sorry (* FIXME: div/mod *)
+lemma "x + (let y = x mod 2 in y + y) < x + (3::int)" by smt
 
 lemma
   assumes "x \<noteq> (0::real)"
@@ -349,7 +347,8 @@
 lemma                                                                         
   assumes "(n + m) mod 2 = 0" and "n mod 4 = 3"                               
   shows "n mod 2 = 1 & m mod 2 = (1::int)"      
-  using assms sorry (* FIXME: div/mod *)
+  using assms by smt
+
 
 
 subsection {* Linear arithmetic with quantifiers *}
@@ -484,10 +483,7 @@
    (eval_dioph ks (map (\<lambda>x. x mod 2) xs) mod 2 = l mod 2 \<and>
     eval_dioph ks (map (\<lambda>x. x div 2) xs) =
       (l - eval_dioph ks (map (\<lambda>x. x mod 2) xs)) div 2)"
-  sorry (* FIXME: div/mod *)
-(*
   by (smt eval_dioph_mod[where n=2] eval_dioph_div_mult[where n=2])
-*)
 
 
 section {* Monomorphization examples *}