doc-src/TutorialI/Ifexpr/ROOT.ML
author narboux
Thu, 15 Feb 2007 18:18:21 +0100
changeset 22326 a3acee47a883
parent 9834 109b11c4e77e
permissions -rw-r--r--
start adding the attribute eqvt to some lemmas of the nominal library

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