src/HOL/MicroJava/ROOT.ML
author kleing
Thu Feb 21 09:54:08 2002 +0100 (2002-02-21)
changeset 12911 704713ca07ea
parent 12786 d655138ddadf
child 12951 a9fdcb71d252
permissions -rw-r--r--
new document
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@10631
    13
use_thy "BVSpecTypeSafe";
kleing@12520
    14
use_thy "JVM";
kleing@12786
    15
kleing@12520
    16
(* momentarily broken:
kleing@12911
    17
use_thy "LBVSpec"; 
kleing@10631
    18
use_thy "LBVCorrect";
kleing@10631
    19
use_thy "LBVComplete";
kleing@12520
    20
*)