src/HOL/MicroJava/BV/Effect.thy
changeset 16558 e97188c6bd71
parent 15481 fc075ae929e4
child 17088 3f797ec16f02