changeset 13505 | 52a16cb7fefb |
parent 13428 | 99e52e78eb65 |
child 13634 | 99a593b49b04 |
--- a/src/ZF/Constructible/Normal.thy Fri Aug 16 12:48:49 2002 +0200 +++ b/src/ZF/Constructible/Normal.thy Fri Aug 16 16:41:48 2002 +0200 @@ -1,3 +1,9 @@ +(* 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*} theory Normal = Main: