nice names for more infix operators

--- a/src/HOL/Tools/res_clause.ML	Wed Sep 14 10:13:12 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML	Wed Sep 14 10:20:50 2005 +0200
@@ -87,7 +87,11 @@
 		   ("op <", "less"),
 		   ("op &", "and"),
 		   ("op |", "or"),
+		   ("op +", "plus"),
+		   ("op -", "minus"),
+		   ("op *", "times"),
 		   ("op -->", "implies"),
+		   ("{}", "emptyset"),
 		   ("op :", "in"),
 		   ("op Un", "union"),
 		   ("op Int", "inter")];