src/HOL/HOLCF/FOCUS/FOCUS.thy
changeset 73473 2cc9bd9a7357
parent 67613 ce654b0e6d69