src/HOL/MicroJava/BV/Effect.thy
changeset 40500 ee9c8d36318e
parent 35440 bdf8ad377877
child 42463 f270e3e18be5