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/SPARK/Tools/spark_vcs.ML
changeset 41635 f938a6022d2e
parent 41561 d1318f3c86ba
child 41878 0778ade00b06 
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Jan 27 12:24:00 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Jan 26 20:51:09 2011 +0100
@@ -287,7 +287,7 @@
       | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop @{const_name sdiv}
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
-      | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name smod}
+      | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name mod}
           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
       | tm_of vs (Funct ("-", [e])) =
isabelle