diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/Rmap.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Induct/Rmap.thy	Wed Nov 07 12:29:07 2001 +0100
@@ -0,0 +1,25 @@
+(*  Title:      ZF/ex/Rmap
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994  University of Cambridge
+
+Inductive definition of an operator to "map" a relation over a list
+*)
+
+Rmap = Main +
+
+consts
+  rmap :: i=>i
+
+inductive
+  domains "rmap(r)" <= "list(domain(r))*list(range(r))"
+  intrs
+    NilI  "<Nil,Nil> \\<in> rmap(r)"
+
+    ConsI "[| <x,y>: r;  <xs,ys> \\<in> rmap(r) |] ==> 
+          <Cons(x,xs), Cons(y,ys)> \\<in> rmap(r)"
+
+  type_intrs "[domainI,rangeI] @ list.intrs"
+
+end
+