src/HOL/MicroJava/ROOT.ML
author berghofe
Mon Dec 10 15:24:22 2001 +0100 (2001-12-10)
changeset 12441 c586d08520ad
parent 11070 cc421547e744
child 12520 6d754b9a1303
permissions -rw-r--r--
Added examples for code generator.
wenzelm@9143
     1
goals_limit := 1;
nipkow@8011
     2
oheimb@10611
     3
add_path "J";
oheimb@10611
     4
add_path "JVM";
oheimb@10611
     5
add_path "BV";
kleing@10631
     6
kleing@10631
     7
use_thy "JTypeSafe";
kleing@10631
     8
use_thy "Example";
berghofe@12441
     9
use_thy "JListExample";
berghofe@12441
    10
use_thy "JVMListExample";
kleing@10631
    11
use_thy "BVSpecTypeSafe";
kleing@10631
    12
use_thy "LBVCorrect";
kleing@10631
    13
use_thy "LBVComplete";
kleing@10631
    14
use_thy "JVM";