author | haftmann |
Wed, 10 Jun 2009 15:04:31 +0200 | |
changeset 31602 | 59df8222c204 |
parent 31601 | 55644fd600c7 |
child 31603 | fa30cd74d7d6 |
--- 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