src/HOL/MicroJava/BV/LBVJVM.thy
changeset 34271 70af06abb13d
parent 34227 33d44b1520c0
child 35416 d8d7d1b785af