src/HOL/MicroJava/BV/EffectMono.thy
changeset 76770 04d7c8496b3d
parent 63258 576fb8068ba6