src/HOL/MicroJava/BV/Effect.thy
changeset 42148 d596e7bb251f
parent 35440 bdf8ad377877
child 42463 f270e3e18be5