doc-src/TutorialI/Ifexpr/ROOT.ML
author boehmes
Mon, 31 Aug 2009 15:29:26 +0200
changeset 32458 de6834b20e9e
parent 9834 109b11c4e77e
permissions -rw-r--r--
sledgehammer's temporary files are removed properly (even in case of an exception occurs)

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