src/HOL/MicroJava/MicroJava.thy
author blanchet
Thu, 14 Apr 2011 11:24:05 +0200
changeset 42348 187354e22c7d
parent 39918 7a1d8b9d17e7
permissions -rw-r--r--
improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)

theory MicroJava
imports
  "J/JTypeSafe"
  "J/Example"
  "J/JListExample"
  "JVM/JVMListExample"
  "JVM/JVMDefensive"
  "BV/LBVJVM"
  "BV/BVNoTypeError"
  "BV/BVExample"
  "Comp/CorrComp"
  "Comp/CorrCompTp"
begin

end