Lines Matching defs:Parse
1 structure Parse :> Parse =
15 val ERROR = mk_HOL_ERR "Parse";
16 val ERRORloc = mk_HOL_ERRloc "Parse";
17 val WARN = HOL_WARNING "Parse"
442 Parse into preterm type
457 Parse into term type.
681 val _ = register_btrace("Parse.unicode_trace_off_complaints",
1147 HOL_WARNING "Parse" "setup_grammars"
1175 add_string "local open GrammarSpecials Parse",
1177 add_string " fun UTOFF f = Feedback.trace(\"Parse.unicode_trace_\
1203 ["val _ = Parse.grammarDB_insert(",Lib.mlquote thyname,",",
1208 ["val _ = Parse.temp_set_grammars ("^
1209 "addtyUDs (Parse.type_grammar()), ",
1210 "addtmUDs (Parse.term_grammar()))"]), NL,
1229 ("Parse.setup_grammars",
1271 HOL_WARNING "Parse" "export_theorems_as_docfiles"
1274 HOL_WARNING "Parse" "export_theorems_as_docfiles"
1307 Theory.register_hook ("Parse.watch_constants", hook)
1348 ("Parse.clear_consts_from_grammar",