src/HOL/MicroJava/BV/LBVJVM.thy
changeset 16558 e97188c6bd71
parent 16417 9bc16273c2d4
child 17090 603f23d71ada