changeset 21416 | f23e4e75dfd3 |
parent 21373 | 18f519614978 |
child 21432 | 625797c592b2 |
--- a/src/HOL/Tools/res_clause.ML Sat Nov 18 00:20:22 2006 +0100 +++ b/src/HOL/Tools/res_clause.ML Sat Nov 18 00:20:24 2006 +0100 @@ -117,7 +117,7 @@ ("HOL.plus", "plus"), ("HOL.minus", "minus"), ("HOL.times", "times"), - ("Divides.op div", "div"), + ("Divides.div", "div"), ("HOL.divide", "divide"), ("op -->", "implies"), ("{}", "emptyset"),