src/HOL/MicroJava/BV/LBVComplete.thy
changeset 9345 2f5f6824f888
parent 9260 678e718a5a86
child 9376 c32c5696ec2a