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
     1 goals_limit := 1;
     2 
     3 add_path "J";
     4 add_path "JVM";
     5 add_path "BV";
     6 
     7 no_document use_thy "While_Combinator";
     8 
     9 use_thy "JTypeSafe";
    10 use_thy "Example";
    11 use_thy "JListExample";
    12 use_thy "JVMListExample";
    13 use_thy "BVSpecTypeSafe";
    14 use_thy "JVM";
    15 
    16 (* momentarily broken:
    17 use_thy "LBVSpec"; 
    18 use_thy "LBVCorrect";
    19 use_thy "LBVComplete";
    20 *)