src/HOL/MicroJava/BV/Effect.thy
changeset 13214 2aa33ed5f526
parent 13066 b57d926d1de2
child 13717 78f91fcdf560