src/HOL/Import/HOL4Compat.thy

--- a/src/HOL/Import/HOL4Compat.thy	Sat Apr 17 20:04:23 2004 +0200
+++ b/src/HOL/Import/HOL4Compat.thy	Sat Apr 17 23:53:35 2004 +0200
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Import/HOL4Compat.thy
+    ID:         $Id$
+    Author:     Sebastian Skalberg (TU Muenchen)
+*)
+
 theory HOL4Compat = HOL4Setup + Divides + Primes + Real:
 
 lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"