src/HOL/MicroJava/BV/Effect.thy
changeset 18260 5597cfcecd49
parent 17090 603f23d71ada
child 18447 da548623916a