creates definitions without typing lemmas. lhs is the new term
constructor and rhs is the what it is defined as. lhs and
rhs are used for the left-hand and right-hand sides of
the abstraction for the new definition.
place is a library position as
described in Chapter 
. lhs is invariably a new term, so you
usually will want to use the new term creation feature of the term
editor to enter it (see Section
). If the opid of the
new definition is id, then utdef adds 2 new objects to the
library starting at position place: