doc-src/IsarRef/Thy/ROOT-HOLCF.ML
author haftmann
Thu, 15 Apr 2010 12:27:14 +0200
changeset 36147 b43b22f63665
parent 32833 f3716d1a2e48
child 37216 3165bc303f66
permissions -rw-r--r--
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl

Unsynchronized.set ThyOutput.source;
use "../../antiquote_setup.ML";

use_thy "HOLCF_Specific";