src/Pure/Tools/ROOT.ML
author paulson
Wed, 19 Jul 2006 11:55:26 +0200
changeset 20153 6ff5d35749b0
parent 20105 454f4be984b7
child 20175 0a8ca32f6e64
permissions -rw-r--r--
Fixed the bugs introduced by the last commit! Output is now *identical* to that produced by the old version, based on a-lists.

(*  Title:      Pure/Tools/ROOT.ML
    ID:         $Id$

Miscellaneous tools and packages for Pure Isabelle.
*)

(*derived theory and proof elements*)
use "invoke.ML";
use "class_package.ML";

(*code generator, 1st generation*)
use "../codegen.ML";

(*code generator, 2nd generation*)
use "codegen_thingol.ML";
use "codegen_serializer.ML";
use "codegen_theorems.ML";
use "codegen_simtype.ML";
use "codegen_package.ML";

(*Steven Obua's evaluator*)
use "am_interpreter.ML";
use "am_compiler.ML";
use "am_util.ML";
use "compute.ML";

(*norm-by-eval*)
use "nbe_eval.ML";
use "nbe_codegen.ML";
use "nbe.ML";