# HG changeset patch
# User paulson
# Date 1126686050 -7200
# Node ID 8727db8f046157b98980d4e269a5c894993a9f9a
# Parent  63e0ab9f2ea95168251bdeee64ed8803918e1c52
nice names for more infix operators

diff -r 63e0ab9f2ea9 -r 8727db8f0461 src/HOL/Tools/res_clause.ML
--- 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")];