src/HOL/MicroJava/BV/Effect.thy
changeset 15789 4cb16144c81b
parent 15481 fc075ae929e4
child 17088 3f797ec16f02