Parse.term_grammar : unit -> term_grammar.grammar
STRUCTURE
SYNOPSIS
Returns the current global term grammar.
LIBRARY
Parse
FAILURE
Never fails.
COMMENTS
There is a pretty-printer installed in the interactive system so that term grammar values are presented nicely. The global term grammar is passed as a parameter to the Term parsing function in the Parse structure, and also drives the installed term and theorem pretty-printers.
SEEALSO
HOL  Kananaskis-13