src/HOL/MicroJava/BV/Effect.thy
changeset 53809 2c0e45bb2f05
parent 46720 9722171731af
child 54863 82acc20ded73