src/HOL/MicroJava/BV/LBVComplete.thy
changeset 9364 e783491b9a1f
parent 9260 678e718a5a86
child 9376 c32c5696ec2a