src/HOL/HOLCF/FOCUS/FOCUS.thy
changeset 66787 64b47495676d
parent 62175 8ffc4d0e652d
child 67613 ce654b0e6d69