# HG changeset patch
# User webertj
# Date 1127484105 -7200
# Node ID 63367feba417c546744a8b24440c2503976fe902
# Parent  a6a322f9614520909f3957c61e2633642fa835f5
header (title/ID) added

diff -r a6a322f96145 -r 63367feba417 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Fri Sep 23 15:45:12 2005 +0200
+++ b/src/HOL/Main.thy	Fri Sep 23 16:01:45 2005 +0200
@@ -1,4 +1,6 @@
-(* $Id$ *)
+(*  Title:      HOL/Main.thy
+    ID:         $Id$
+*)
 
 header {* Main HOL *}