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"