src/HOL/HOLCF/FOCUS/FOCUS.thy
changeset 74684 df1b9f63b2be
parent 67613 ce654b0e6d69