changeset 32135 | f645b51e8e54 |
parent 31910 | a8e9ccfc427a |
child 32264 | 0be31453f698 |
--- a/src/HOL/Tools/res_clause.ML Wed Jul 22 14:20:32 2009 +0200 +++ b/src/HOL/Tools/res_clause.ML Wed Jul 22 14:20:32 2009 +0200 @@ -110,8 +110,8 @@ (@{const_name "op -->"}, "implies"), (@{const_name Set.empty}, "emptyset"), (@{const_name "op :"}, "in"), - (@{const_name Un}, "union"), - (@{const_name Int}, "inter"), + (@{const_name union}, "union"), + (@{const_name inter}, "inter"), ("List.append", "append"), ("ATP_Linkup.fequal", "fequal"), ("ATP_Linkup.COMBI", "COMBI"),