diff -r b03a36b8d528 -r 99a593b49b04 src/ZF/Constructible/Normal.thy --- a/src/ZF/Constructible/Normal.thy Tue Oct 08 14:09:18 2002 +0200 +++ b/src/ZF/Constructible/Normal.thy Wed Oct 09 11:07:13 2002 +0200 @@ -1,7 +1,6 @@ (* Title: ZF/Constructible/Normal.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge *) header {*Closed Unbounded Classes and Normal Functions*}