src/HOL/MicroJava/BV/Effect.thy
changeset 49486 64cc57c0d0fe
parent 46720 9722171731af
child 54863 82acc20ded73