src/HOL/HOLCF/FOCUS/FOCUS.thy
changeset 69205 8050734eee3e
parent 67613 ce654b0e6d69