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