src/HOL/MicroJava/BV/Effect.thy
changeset 47327 600e6b07a693
parent 46720 9722171731af
child 54863 82acc20ded73