doc-src/Tutorial/Misc/tree
author wenzelm
Tue, 26 Feb 2002 21:46:03 +0100
changeset 12958 99f5c4a37b29
parent 5377 efb799c5ed3c
permissions -rw-r--r--
added smart_have_thmss (global storage); removed add_thmss_hybrid; clarified add_thmss;

datatype 'a tree = Tip | Node ('a tree) 'a ('a tree)