--- a/src/ZF/ex/Rmap.thy Wed Nov 07 00:16:19 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(* 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
-