Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Removed div/mod ML code because it fails for 0.
authornipkow
Mon, 17 Jan 2005 15:21:40 +0100
changeset 15440 d0cd75f7a365
parent 15439 71c0f98e31f1
child 15441 42b858b978b8
Removed div/mod ML code because it fails for 0.
src/HOL/Integ/NatBin.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/NatBin.thy	Fri Jan 14 12:00:27 2005 +0100
+++ b/src/HOL/Integ/NatBin.thy	Mon Jan 17 15:21:40 2005 +0100
@@ -848,8 +848,10 @@
   "uminus" :: "int => int"      ("`~")
   "op +" :: "int => int => int" ("(_ `+/ _)")
   "op *" :: "int => int => int" ("(_ `*/ _)")
+(* Fails for 0:
   "op div" :: "int => int => int" ("(_ div/ _)")
   "op mod" :: "int => int => int" ("(_ mod/ _)")
+*)
   "op <" :: "int => int => bool" ("(_ </ _)")
   "op <=" :: "int => int => bool" ("(_ <=/ _)")
   "neg"                         ("(_ < 0)")
isabelle