doc-src/TutorialI/Ifexpr/ROOT.ML
author webertj
Thu, 17 Mar 2005 01:40:18 +0100
changeset 15611 c01f11cd08f9
parent 9834 109b11c4e77e
permissions -rw-r--r--
Bugfix related to the interpretation of IDT constructors

use "../settings.ML";
use_thy "Ifexpr";