doc-src/TutorialI/Ifexpr/ROOT.ML
author paulson
Thu, 27 Sep 2007 17:55:28 +0200
changeset 24742 73b8b42a36b6
parent 9834 109b11c4e77e
permissions -rw-r--r--
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering theorems of Nat.thy are hidden by the Ordering.thy versions

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