src/HOL/MicroJava/BV/LBVJVM.thy
changeset 26618 f3535afb58e8
parent 26450 158b924b5153
child 27681 8cedebf55539