doc-src/TutorialI/ToyList2/ROOT.ML
author huffman
Fri, 04 Nov 2011 08:00:48 +0100
changeset 45335 a68ce51de69a
parent 8745 13b32661dde4
permissions -rw-r--r--
ex/Tree23.thy: simplify proof of bal_del0

use_thy "ToyList";