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