Re: [isabelle] beginner doubt: how can I evaluate a function?

The `value' command that John Matthews mentioned has been available since the 2005 version.


Simone Cavalheiro schrieb:
I have just started using and learning Isabelle and
I am trying to evaluate basic functions as, for example, "rev [1::nat, 2 ,
3]". I have done it using
ML code (command ML), but I would like to define my own functions inside a
theory and evaluate them (just to test) before proving some property.
How it can be done inside a theory?

Sorry for the basic question.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.