src/Pure/Tools/ROOT.ML
author haftmann
Fri, 17 Mar 2006 14:19:24 +0100
changeset 19280 5091dc43817b
parent 19147 0f584853b6a4
child 19341 3414c04fbc39
permissions -rw-r--r--
slight improvement in serializer, stub for code generator theorems added
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
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
     7
(*class package*)
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
     8
use "class_package.ML";
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
     9
19280
5091dc43817b slight improvement in serializer, stub for code generator theorems added
haftmann
parents: 19147
diff changeset
    10
(*code generator theorems*)
5091dc43817b slight improvement in serializer, stub for code generator theorems added
haftmann
parents: 19147
diff changeset
    11
use "codegen_theorems.ML";
5091dc43817b slight improvement in serializer, stub for code generator theorems added
haftmann
parents: 19147
diff changeset
    12
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    13
(*code generator, 1st generation*)
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    14
use "../codegen.ML";
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    15
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    16
(*code generator, 2nd generation*)
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    17
use "codegen_thingol.ML";
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    18
use "codegen_serializer.ML";
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    19
use "codegen_package.ML";
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    20
16842
wenzelm
parents: 16781
diff changeset
    21
(*Steven Obua's evaluator*)
16781
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
    22
use "am_interpreter.ML";
16842
wenzelm
parents: 16781
diff changeset
    23
use "am_compiler.ML";
16781
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
    24
use "am_util.ML";
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
    25
use "compute.ML";
19118
52f751b50716 added Tools/nbe, fixes
nipkow
parents: 18169
diff changeset
    26
52f751b50716 added Tools/nbe, fixes
nipkow
parents: 18169
diff changeset
    27
(* norm-by-eval *)
52f751b50716 added Tools/nbe, fixes
nipkow
parents: 18169
diff changeset
    28
use "nbe_eval.ML";
52f751b50716 added Tools/nbe, fixes
nipkow
parents: 18169
diff changeset
    29
use "nbe_codegen.ML";
19147
0f584853b6a4 added nbe, updated neb_*
nipkow
parents: 19118
diff changeset
    30
use "nbe.ML";