header {* Prefixpoints *}

theory Ex4
imports LCF
begin

end