src/Pure/Tools/ROOT.ML
author haftmann
Sat, 10 Feb 2007 09:26:17 +0100
changeset 22298 9ca7d368968d
parent 22208 2d6e8cf48670
child 22744 5cbe966d67a2
permissions -rw-r--r--
added class package to Isar bootstrap

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

Miscellaneous tools and packages for Pure Isabelle.
*)

(*XML syntax for terms and types*)
use "xml_syntax.ML";

(*derived theory and proof elements*)
use "invoke.ML";
(* use "class_package.ML"; see Pure/Isar/ROOT.ML *)

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

(*code generator, 2nd generation*)
use "codegen_consts.ML";
use "codegen_func.ML";
use "codegen_data.ML";
use "codegen_names.ML";
use "codegen_funcgr.ML";
use "codegen_thingol.ML";
use "codegen_serializer.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";