src/HOL/MicroJava/ROOT.ML
author streckem
Wed, 23 Oct 2002 16:09:02 +0200
changeset 13672 b95d12325b51
parent 13632 c7cbb2b369b8
child 24073 373727835757
permissions -rw-r--r--
Added compiler
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9143
6180c29d2db6 use with_paths;
wenzelm
parents: 9000
diff changeset
     1
goals_limit := 1;
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     2
10611
e460c53c1c9b simplified interactive handling
oheimb
parents: 10047
diff changeset
     3
add_path "J";
e460c53c1c9b simplified interactive handling
oheimb
parents: 10047
diff changeset
     4
add_path "JVM";
e460c53c1c9b simplified interactive handling
oheimb
parents: 10047
diff changeset
     5
add_path "BV";
13672
b95d12325b51 Added compiler
streckem
parents: 13632
diff changeset
     6
add_path "Comp";
10631
591ea23d27a0 removed Digest (temporarily, not up to date)
kleing
parents: 10611
diff changeset
     7
12911
704713ca07ea new document
kleing
parents: 12786
diff changeset
     8
no_document use_thy "While_Combinator";
704713ca07ea new document
kleing
parents: 12786
diff changeset
     9
10631
591ea23d27a0 removed Digest (temporarily, not up to date)
kleing
parents: 10611
diff changeset
    10
use_thy "JTypeSafe";
591ea23d27a0 removed Digest (temporarily, not up to date)
kleing
parents: 10611
diff changeset
    11
use_thy "Example";
12441
c586d08520ad Added examples for code generator.
berghofe
parents: 11070
diff changeset
    12
use_thy "JListExample";
12522
69971d68fe03 fixed JVMListExample
kleing
parents: 12520
diff changeset
    13
use_thy "JVMListExample";
13632
c7cbb2b369b8 defensive machine
kleing
parents: 13215
diff changeset
    14
use_thy "JVMDefensive";
13215
072a77989ce0 LBV instantiated for JVM
kleing
parents: 13072
diff changeset
    15
use_thy "LBVJVM";
13632
c7cbb2b369b8 defensive machine
kleing
parents: 13215
diff changeset
    16
use_thy "BVNoTypeError";
12951
a9fdcb71d252 introduces SystemClasses and BVExample
kleing
parents: 12911
diff changeset
    17
use_thy "BVExample";
13672
b95d12325b51 Added compiler
streckem
parents: 13632
diff changeset
    18
b95d12325b51 Added compiler
streckem
parents: 13632
diff changeset
    19
use_thy "CorrComp";
b95d12325b51 Added compiler
streckem
parents: 13632
diff changeset
    20
use_thy "CorrCompTp";