changeset 18676 | 5bce9fddce2e |
parent 18449 | e314fb38307d |
child 18798 | ca02a2077955 |
--- a/src/HOL/Tools/res_clause.ML Fri Jan 13 17:39:03 2006 +0100 +++ b/src/HOL/Tools/res_clause.ML Fri Jan 13 17:39:19 2006 +0100 @@ -120,6 +120,8 @@ ("op +", "plus"), ("op -", "minus"), ("op *", "times"), + ("Divides.op div", "div"), + ("HOL.divide", "divide"), ("op -->", "implies"), ("{}", "emptyset"), ("op :", "in"),