src/HOL/MicroJava/BV/Effect.thy
changeset 39758 b8a53e3a0ee2
parent 35440 bdf8ad377877
child 42463 f270e3e18be5