1.1 --- a/src/HOL/SMT/Examples/SMT_Examples.thy	Fri Nov 06 17:52:57 2009 +0100
     1.2 +++ b/src/HOL/SMT/Examples/SMT_Examples.thy	Wed Nov 18 09:34:53 2009 +0100
     1.3 @@ -409,6 +409,13 @@
     1.4    using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_linarith_20"]]
     1.5    by smt
     1.6  
     1.7 +lemma                                                                         
     1.8 +  assumes "(n + m) mod 2 = 0" and "n mod 4 = 3"                               
     1.9 +  shows "n mod 2 = 1 & m mod 2 = (1::int)"      
    1.10 +  using assms
    1.11 +  using [[smt_cert="$ISABELLE_SMT/Examples/cert/z3_linarith_21"]]
    1.12 +  by smt
    1.13 +
    1.14  
    1.15  subsection {* Linear arithmetic with quantifiers *}
    1.16