src/HOLCF/ex/Focus_ex.thy
changeset 20192 956cd30ef3be
parent 19763 ec18656a2c10
child 21404 eb85850d3eb7