src/Pure/Tools/ROOT.ML
author haftmann
Fri, 05 Jan 2007 14:32:07 +0100
changeset 22023 487b79b95a20
parent 20939 a81ce849e9f4
child 22208 2d6e8cf48670
permissions -rw-r--r--
added codegen_func.ML
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
20708
29c1754b250f changed order
haftmann
parents: 20657
diff changeset
     7
19812
60c6bfbf6ca1 added invoke.ML;
wenzelm
parents: 19341
diff changeset
     8
(*derived theory and proof elements*)
60c6bfbf6ca1 added invoke.ML;
wenzelm
parents: 19341
diff changeset
     9
use "invoke.ML";
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    10
use "class_package.ML";
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    11
19341
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19280
diff changeset
    12
(*code generator, 1st generation*)
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19280
diff changeset
    13
use "../codegen.ML";
3414c04fbc39 added definitional code generator module: codegen_theorems.ML
haftmann
parents: 19280
diff changeset
    14
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    15
(*code generator, 2nd generation*)
20384
049d955cf716 added code generator packages
haftmann
parents: 20353
diff changeset
    16
use "codegen_consts.ML";
22023
487b79b95a20 added codegen_func.ML
haftmann
parents: 20939
diff changeset
    17
use "codegen_func.ML";
20708
29c1754b250f changed order
haftmann
parents: 20657
diff changeset
    18
use "codegen_data.ML";
20353
d73e49780ef2 code generator refinements
haftmann
parents: 20175
diff changeset
    19
use "codegen_names.ML";
20600
6d75e02ed285 added codegen_data
haftmann
parents: 20384
diff changeset
    20
use "codegen_funcgr.ML";
18169
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    21
use "codegen_thingol.ML";
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    22
use "codegen_serializer.ML";
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    23
use "codegen_package.ML";
45def66f86cb added modules for code generator generation two, not operational yet
haftmann
parents: 16842
diff changeset
    24
16842
wenzelm
parents: 16781
diff changeset
    25
(*Steven Obua's evaluator*)
16781
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
    26
use "am_interpreter.ML";
16842
wenzelm
parents: 16781
diff changeset
    27
use "am_compiler.ML";
16781
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
    28
use "am_util.ML";
663235466562 - introduce Pure/Tools directory
obua
parents:
diff changeset
    29
use "compute.ML";
19118
52f751b50716 added Tools/nbe, fixes
nipkow
parents: 18169
diff changeset
    30
19812
60c6bfbf6ca1 added invoke.ML;
wenzelm
parents: 19341
diff changeset
    31
(*norm-by-eval*)
19118
52f751b50716 added Tools/nbe, fixes
nipkow
parents: 18169
diff changeset
    32
use "nbe_eval.ML";
52f751b50716 added Tools/nbe, fixes
nipkow
parents: 18169
diff changeset
    33
use "nbe_codegen.ML";
19147
0f584853b6a4 added nbe, updated neb_*
nipkow
parents: 19118
diff changeset
    34
use "nbe.ML";
20657
da6e410c5387 Added xml_syntax.ML
berghofe
parents: 20600
diff changeset
    35
da6e410c5387 Added xml_syntax.ML
berghofe
parents: 20600
diff changeset
    36
(*XML syntax for terms and types*)
da6e410c5387 Added xml_syntax.ML
berghofe
parents: 20600
diff changeset
    37
use "xml_syntax.ML";