src/HOL/MicroJava/MicroJava.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 39918 7a1d8b9d17e7
permissions -rw-r--r--
specialized specification: avoid trivial instances
haftmann@27680
     1
theory MicroJava
haftmann@27680
     2
imports
haftmann@27680
     3
  "J/JTypeSafe"
haftmann@27680
     4
  "J/Example"
haftmann@27680
     5
  "J/JListExample"
haftmann@27680
     6
  "JVM/JVMListExample"
haftmann@27680
     7
  "JVM/JVMDefensive"
haftmann@27680
     8
  "BV/LBVJVM"
haftmann@27680
     9
  "BV/BVNoTypeError"
haftmann@27680
    10
  "BV/BVExample"
haftmann@27680
    11
  "Comp/CorrComp"
haftmann@27680
    12
  "Comp/CorrCompTp"
haftmann@27680
    13
begin
haftmann@27680
    14
haftmann@39918
    15
end