next up previous contents index
Next: The Metalanguage Up: The Rules Previous: UNIVERSE

MISCELLANEOUS

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* hypothesis hyp(hyp): int rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* sequence seq(term_list id_list): (term list) (tok list) rule.
where the length of the token list should match the length of the term list.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* lemma lemma(lemma_name x): tok tok rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* def def(theorem x): tok tok rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* explicit intro explicit_intro(term): term rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* cumulativity cumulativity(level): int rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* substitution substitution(level equality_term over_id over): int term tok term rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* direct computation direct_computation(tagged_term): term rule.

direct_computation_hyp(hyp tagged_term): int term rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* equality equality: rule.

mlsubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* arith arith(level): int rule.

}


Richard Eaton
Thu Sep 14 08:45:18 EDT 1995