src/HOL/Tools/SMT/smt_normalize.ML
changeset 44890 22f665a2e91c
parent 44718 b656af4c9796
child 46497 89ccf66aa73d
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -475,7 +475,7 @@
     1.4      "op * = (%a b. nat (int a * int b))"
     1.5      "op div = (%a b. nat (int a div int b))"
     1.6      "op mod = (%a b. nat (int a mod int b))"
     1.7 -    by (fastsimp simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
     1.8 +    by (fastforce simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
     1.9  
    1.10    val ints = map mk_meta_eq @{lemma
    1.11      "int 0 = 0"