changeset 15440 | d0cd75f7a365 |
parent 15439 | 71c0f98e31f1 |
child 15531 | 08c8dad8e399 |
--- 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)")