src/ZF/Coind/Types.thy
changeset 46822 95f1e700b712
parent 35762 af3ff2ba4c54
child 76213 e44d86131648
--- a/src/ZF/Coind/Types.thy	Tue Mar 06 16:06:52 2012 +0000
+++ b/src/ZF/Coind/Types.thy	Tue Mar 06 16:46:27 2012 +0000
@@ -30,7 +30,7 @@
 
 primrec (*domain of the type environment*)
   "te_dom (te_emp) = 0"
-  "te_dom (te_owr(te,x,v)) = te_dom(te) Un {x}"
+  "te_dom (te_owr(te,x,v)) = te_dom(te) \<union> {x}"
 
 primrec (*lookup up identifiers in the type environment*)
   "te_app (te_emp,x) = 0"