changeset 13505 | 52a16cb7fefb |
parent 13434 | 78b93a667c01 |
child 13563 | 7d6c9817c432 |
--- a/src/ZF/Constructible/Reflection.thy Fri Aug 16 12:48:49 2002 +0200 +++ b/src/ZF/Constructible/Reflection.thy Fri Aug 16 16:41:48 2002 +0200 @@ -1,3 +1,9 @@ +(* Title: ZF/Constructible/Reflection.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2002 University of Cambridge +*) + header {* The Reflection Theorem*} theory Reflection = Normal: