changeset 1478 | 2b8c2a7547ab |
parent 1401 | 0c439768f45c |
child 3840 | e0baea4d485a |
--- a/src/ZF/ex/Rmap.thy Mon Feb 05 21:33:14 1996 +0100 +++ b/src/ZF/ex/Rmap.thy Tue Feb 06 12:27:17 1996 +0100 @@ -1,6 +1,6 @@ -(* Title: ZF/ex/Rmap +(* Title: ZF/ex/Rmap ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + 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