src/HOL/HOLCF/FOCUS/FOCUS.thy
changeset 73568 bdba138d462d
parent 67613 ce654b0e6d69