src/HOL/MicroJava/ROOT.ML
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24073 373727835757
child 27680 5a557a5afc48
permissions -rw-r--r--
Name.uu, Name.aT;
wenzelm@24073
     1
(* $Id$ *)
kleing@10631
     2
kleing@12911
     3
no_document use_thy "While_Combinator";
kleing@12911
     4
wenzelm@24073
     5
use_thys ["J/JTypeSafe", "J/Example", "J/JListExample",
wenzelm@24073
     6
  "JVM/JVMListExample", "JVM/JVMDefensive", "BV/LBVJVM",
wenzelm@24073
     7
  "BV/BVNoTypeError", "BV/BVExample", "Comp/CorrComp",
wenzelm@24073
     8
  "Comp/CorrCompTp"];