changeset 3841 | 22bbc1676768 |
parent 3840 | e0baea4d485a |
child 11316 | b4e71bd751e4 |
--- a/src/ZF/ex/Rmap.thy Fri Oct 10 18:23:31 1997 +0200 +++ b/src/ZF/ex/Rmap.thy Fri Oct 10 18:37:49 1997 +0200 @@ -19,7 +19,7 @@ ConsI "[| <x,y>: r; <xs,ys> : rmap(r) |] ==> <Cons(x,xs), Cons(y,ys)> : rmap(r)" - type_intrs "[domainI,rangeI] @ list. intrs" + type_intrs "[domainI,rangeI] @ list.intrs" end