src/HOL/MicroJava/BV/EffectMono.thy
changeset 13717 78f91fcdf560
parent 13601 fd3e3d6b37b2
child 13718 9f94248d2f5a