inner syntax comments may be written as "\<comment> \<open>text\<close>";
(* Title: HOL/HOLCF/HOLCF.thy Author: Franz Regensburger Author: Brian HuffmanHOLCF -- a semantic extension of HOL by the LCF logic.*)theory HOLCFimports Main Domain Powerdomainsbegindefault_sort "domain"end