src/HOL/HOLCF/ex/Focus_ex.thy
changeset 56065 600781e03bf6
parent 55381 ca31f042414f
child 62175 8ffc4d0e652d