doc-src/TutorialI/Misc/ROOT.ML
author webertj
Mon, 12 Jan 2004 14:35:07 +0100
changeset 14351 cd3ef10d02be
parent 13305 f88d0c363582
permissions -rw-r--r--
Fixed compatibility issues with SML/NJ: - replaced '(op *)' by 'op*' - replaced 'LargeInt' by 'Int'

use "../settings.ML";
use_thy "Tree";
use_thy "Tree2";
use_thy "Plus";
use_thy "case_exprs";
use_thy "fakenat";
use_thy "natsum";
use_thy "pairs";
use_thy "Option2";
use_thy "types";
use_thy "prime_def";
use_thy "simp";
use_thy "Itrev";
use_thy "AdvancedInd";
use_thy "appendix";