src/HOL/MicroJava/ROOT.ML
author wenzelm
Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039 a901bafe4578
parent 8011 d14c4e9e9c8e
child 9000 c20d58286a51
permissions -rw-r--r--
Goal: tuned pris;
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";