src/HOL/MicroJava/JVM/JVMDefensive.thy
changeset 13676 b1915d3e571d
parent 13631 23ab136db946
child 13677 5fad004bd9df