Lines Matching refs:help
158 " For introductory HOL help, type: help \"hol\";\n" ^164 * Set up the help paths. *165 * Set parameters for parsing and help. *183 ( hol_use ("help" ++ "src-sml") "Database"197 fun HELP s = path (HOLDIR ++ "help" ++ s)203 {file = "help" ++ "Docfiles" ++ "HOL.help",209 val help = Help.help