src/HOL/MicroJava/BV/LBVCorrect.thy
changeset 26964 df1f238a05f7
parent 23464 bc2563c37b1a
child 27681 8cedebf55539