Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/SMT/smt_normalize.ML
changeset 44890 22f665a2e91c
parent 44718 b656af4c9796
child 46497 89ccf66aa73d 
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 12 07:55:43 2011 +0200
@@ -475,7 +475,7 @@
     "op * = (%a b. nat (int a * int b))"
     "op div = (%a b. nat (int a div int b))"
     "op mod = (%a b. nat (int a mod int b))"
-    by (fastsimp simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
+    by (fastforce simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
 
   val ints = map mk_meta_eq @{lemma
     "int 0 = 0"
isabelle