src/HOL/MicroJava/ROOT.ML
author nipkow
Fri, 26 Nov 1999 08:46:59 +0100
changeset 8034 6fc37b5c5e98
parent 8011 d14c4e9e9c8e
child 9000 c20d58286a51
permissions -rw-r--r--
Various little changes like cmethd -> method and cfield -> field.
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";