src/ZF/ex/Contract0.thy
changeset 16 0b033d50ca1c
parent 0 a5a9c433f639
     1.1 --- a/src/ZF/ex/Contract0.thy	Thu Sep 30 10:26:38 1993 +0100
     1.2 +++ b/src/ZF/ex/Contract0.thy	Thu Sep 30 10:54:01 1993 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title: 	ZF/ex/contract.thy
     1.5      ID:         $Id$
     1.6 -    Author: 	Tobias Nipkow & Lawrence C Paulson
     1.7 +    Author: 	Lawrence C Paulson
     1.8      Copyright   1993  University of Cambridge
     1.9  
    1.10  Inductive definition of (1-step) contractions and (mult-step) reductions