src/HOL/Tools/res_clause.ML

 		   ("op *", "times"),
 		   ("op -->", "implies"),
 		   ("{}", "emptyset"),
 		   ("op :", "in"),
 		   ("op Un", "union"),
-		   ("op Int", "inter")];
+		   ("op Int", "inter"),
+		   ("List.op @", "append")];
 
 val type_const_trans_table =
       Symtab.make [("*", "t_prod"),
 	  	   ("+", "t_sum"),
 		   ("~=>", "t_map")];