# HG changeset patch
# User haftmann
# Date 1244639071 -7200
# Node ID 59df8222c2041a380cbdbbf44ec13869a37f1ab1
# Parent  55644fd600c701cd93a81d7035eea1e5c84f6084
tuned header

diff -r 55644fd600c7 -r 59df8222c204 src/HOL/Induct/Tree.thy
--- a/src/HOL/Induct/Tree.thy	Wed Jun 10 10:09:30 2009 +0200
+++ b/src/HOL/Induct/Tree.thy	Wed Jun 10 15:04:31 2009 +0200
@@ -1,12 +1,13 @@
 (*  Title:      HOL/Induct/Tree.thy
-    ID:         $Id$
     Author:     Stefan Berghofer,  TU Muenchen
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
 header {* Infinitely branching trees *}
 
-theory Tree imports Main begin
+theory Tree
+imports Main
+begin
 
 datatype 'a tree =
     Atom 'a