doc-src/TutorialI/Misc/Tree.thy

 (*<*)
-theory Tree = Main:
+theory Tree imports Main begin
 (*>*)
 
 text{*\noindent
 Define the datatype of \rmindex{binary trees}:
 *}