src/HOL/MicroJava/ROOT.ML
author kleing
Thu Dec 07 19:26:30 2000 +0100 (2000-12-07)
changeset 10631 591ea23d27a0
parent 10611 e460c53c1c9b
child 11026 a50365d21144
permissions -rw-r--r--
removed Digest (temporarily, not up to date)
added theory JVM
wenzelm@9000
     1
wenzelm@9143
     2
goals_limit := 1;
nipkow@8011
     3
nipkow@8011
     4
Unify.search_bound := 40;
nipkow@8011
     5
Unify.trace_bound  := 40;
nipkow@8011
     6
oheimb@10611
     7
add_path "J";
oheimb@10611
     8
add_path "JVM";
oheimb@10611
     9
add_path "BV";
kleing@10631
    10
kleing@10631
    11
use_thy "JTypeSafe";
kleing@10631
    12
use_thy "Example";
kleing@10631
    13
use_thy "BVSpecTypeSafe";
kleing@10631
    14
use_thy "LBVCorrect";
kleing@10631
    15
use_thy "LBVComplete";
kleing@10631
    16
use_thy "JVM";