src/HOL/MicroJava/BV/Effect.thy
changeset 48980 debfa361f648
parent 46720 9722171731af
child 54863 82acc20ded73