src/HOL/MicroJava/ROOT.ML
author berghofe
Wed, 21 May 2008 14:04:41 +0200
changeset 26964 df1f238a05f7
parent 24073 373727835757
child 27680 5a557a5afc48
permissions -rw-r--r--
Added entry explaining incompatibilities introduced by replacing sets by predicates.

(* $Id$ *)

no_document use_thy "While_Combinator";

use_thys ["J/JTypeSafe", "J/Example", "J/JListExample",
  "JVM/JVMListExample", "JVM/JVMDefensive", "BV/LBVJVM",
  "BV/BVNoTypeError", "BV/BVExample", "Comp/CorrComp",
  "Comp/CorrCompTp"];