src/HOL/MicroJava/BV/LBVCorrect.thy
changeset 9000 c20d58286a51
parent 8390 e5b618f6824e
child 9012 d1bd2144ab5d