Lines Matching defs:prefix
565 fun pp_hol_as_tex_command prefix (s, thm) =
567 val es = prefix ^ tex_command_escape s
593 let val prefix = datatype_prefix()
598 map (pp_hol_as_tex_command prefix) thms @
599 [pp_newcommand prefix, NL] @
600 map (pp_hol_as_tex prefix o fst) thms @
606 let val prefix = definition_prefix()
611 map (pp_hol_as_tex_command prefix) thms @
612 [pp_newcommand prefix, NL] @
613 map (pp_hol_as_tex_with_tag (prefix, "HOLDfnTag") o fst) thms @
619 let val prefix = theorem_prefix()
624 map (pp_hol_as_tex_command prefix) thms @
625 [pp_newcommand prefix, NL] @
626 map (pp_hol_as_tex_with_tag (prefix, "HOLThmTag") o fst) thms @