changeset 18390 | aaecdaef4c04 |
parent 18275 | 86cefba6d325 |
child 18402 | aaba095cf62b |
--- a/src/HOL/Tools/res_clause.ML Tue Dec 13 15:27:43 2005 +0100 +++ b/src/HOL/Tools/res_clause.ML Tue Dec 13 15:34:02 2005 +0100 @@ -113,7 +113,8 @@ ("{}", "emptyset"), ("op :", "in"), ("op Un", "union"), - ("op Int", "inter")]; + ("op Int", "inter"), + ("List.op @", "append")]; val type_const_trans_table = Symtab.make [("*", "t_prod"),