src/HOL/MicroJava/BV/Effect.thy
changeset 17012 036c46df9576
parent 15481 fc075ae929e4
child 17088 3f797ec16f02