src/Pure/Tools/ROOT.ML
author wenzelm
Mon, 29 Aug 2005 16:18:04 +0200
changeset 17184 3d80209e9a53
parent 16842 5979c46853d1
child 18169 45def66f86cb
permissions -rw-r--r--
use AList operations;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16781
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
     1
(*  Title:      Pure/Tools/ROOT.ML
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
     2
    ID:         $Id$
16842
wenzelm
parents: 16781
diff changeset
     3
wenzelm
parents: 16781
diff changeset
     4
Miscellaneous tools and packages for Pure Isabelle.
16781
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
     5
*)
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
     6
16842
wenzelm
parents: 16781
diff changeset
     7
(*Steven Obua's evaluator*)
16781
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
     8
use "am_interpreter.ML";
16842
wenzelm
parents: 16781
diff changeset
     9
use "am_compiler.ML";
16781
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
    10
use "am_util.ML";
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
    11
use "compute.ML";