src/ZF/ex/Rmap.thy
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