src/HOL/MicroJava/ROOT.ML
author kleing
Tue Feb 26 15:45:32 2002 +0100 (2002-02-26)
changeset 12951 a9fdcb71d252
parent 12911 704713ca07ea
child 12978 16cc829b9c65
permissions -rw-r--r--
introduces SystemClasses and BVExample
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@12911
     7
no_document use_thy "While_Combinator";
kleing@12911
     8
kleing@10631
     9
use_thy "JTypeSafe";
kleing@10631
    10
use_thy "Example";
berghofe@12441
    11
use_thy "JListExample";
kleing@12522
    12
use_thy "JVMListExample";
kleing@12951
    13
use_thy "JVM";
kleing@10631
    14
use_thy "BVSpecTypeSafe";
kleing@12951
    15
use_thy "BVExample";
kleing@12786
    16
kleing@12520
    17
(* momentarily broken:
kleing@12911
    18
use_thy "LBVSpec"; 
kleing@10631
    19
use_thy "LBVCorrect";
kleing@10631
    20
use_thy "LBVComplete";
kleing@12520
    21
*)