src/HOL/MicroJava/BV/LBVCorrect.thy
changeset 9348 f495dba0cb07
parent 9260 678e718a5a86
child 9376 c32c5696ec2a