Isabelle definitions [isa-001G]

The Isabelle definition command is a safer way to define constants than the axiomatization command. The syntax is similiar:

definition my_const :: "type" where (* equation *)

However, there are several differences:

• Only one constant (my_const above) can be defined.
• Only one axiom can be defined, and it must be an equation of the format my_const ... = ..., describing the meaning of my_const in terms of other, already-defined constants.

If no name is given to the defining equation, the default name produced by appending _def to the name of the constant is used (e.g. my_const_def)