src/ZF/Constructible/Reflection.thy
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: