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/z3_interface.ML
changeset 63950 cdc1e59aa513
parent 60352 d46de31a50c4
child 66551 4df6b0ae900d 
--- a/src/HOL/Tools/SMT/z3_interface.ML	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Mon Sep 26 07:56:54 2016 +0200
@@ -35,7 +35,7 @@
      serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
 
   fun is_div_mod @{const divide (int)} = true
-    | is_div_mod @{const mod (int)} = true
+    | is_div_mod @{const modulo (int)} = true
     | is_div_mod _ = false
 
   val have_int_div_mod = exists (Term.exists_subterm is_div_mod o Thm.prop_of)
isabelle