src/HOL/MicroJava/ROOT.ML
author wenzelm
Thu, 16 Mar 2000 00:32:55 +0100
changeset 8488 58e37d59c146
parent 8011 d14c4e9e9c8e
child 9000 c20d58286a51
permissions -rw-r--r--
do not change parindent/parskip;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     1
goals_limit:=1;
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     2
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     3
Unify.search_bound := 40;
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     4
Unify.trace_bound  := 40;
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     5
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     6
add_path "J";
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     7
add_path "JVM";
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     8
add_path "BV";
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     9
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    10
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    11
use_thy "JTypeSafe";
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    12
use_thy "BVSpecTypeSafe";