Lines Matching refs:to
17 [define_tyop r] will be called when the article wants to define a type. [r]
18 consists of the name of the type operator to be defined, the type axiom, a list
26 [define_const name rhs] will be called when the article wants to define a new
30 [axiom thms (h,c)] will be called when the article wants to retrieve an
35 [const_name n] and [tyop_name n] will be called to translate OpenTheory names
36 to HOL4 names. The following functions can be used to simply look the names up in the global OpenTheory map.
43 An axiom function for readers that tries to find the desired theorem in the
54 define_tyop and define_const functions for readers that try to produce the
57 current theory. The first argument to [define_const_in_thy] is a function to