src/HOL/MicroJava/BV/Effect.thy
changeset 36260 c0ab79a100e4
parent 35440 bdf8ad377877
child 42463 f270e3e18be5