Mercurial Mercurial > repos > isabelle / comparison
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 63950 cdc1e59aa513
parent 63352 4eaf35781b23
child 64574 1134e4d5e5b7
equal deleted inserted replaced
63949:e7e41db7221b 63950:cdc1e59aa513 
   439           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
   439           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
   440 
   440 
   441       | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop @{const_name sdiv}
 
   441       | tm_of vs (Funct ("div", [e, e'])) = (HOLogic.mk_binop @{const_name sdiv}
 
   442           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
   442           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
   443 
   443 
   444       | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name mod}
 
   444       | tm_of vs (Funct ("mod", [e, e'])) = (HOLogic.mk_binop @{const_name modulo}
 
   445           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
   445           (fst (tm_of vs e), fst (tm_of vs e')), integerN)
 
   446 
   446 
   447       | tm_of vs (Funct ("-", [e])) =
 
   447       | tm_of vs (Funct ("-", [e])) =
 
   448           (mk_unop @{const_name uminus} (fst (tm_of vs e)), integerN)
 
   448           (mk_unop @{const_name uminus} (fst (tm_of vs e)), integerN)
 
   449 
   449
isabelle