*To*: Simone Cavalheiro <simone.cavalheiro at gmail.com>*Subject*: Re: [isabelle] beginner doubt: how can I evaluate a function?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 05 Oct 2007 09:08:16 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <43810af60710030743k14845b56l880ed42113c0b763@mail.gmail.com>*References*: <43810af60710030743k14845b56l880ed42113c0b763@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.0 (Macintosh/20070326)

Tobias 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. Simone

**References**:**[isabelle] beginner doubt: how can I evaluate a function?***From:*Simone Cavalheiro

- Previous by Date: Re: [isabelle] Extra type variables in constdef
- Next by Date: [isabelle] 2nd CFP: Systems Software Verification 2008
- Previous by Thread: Re: [isabelle] beginner doubt: how can I evaluate a function?
- Next by Thread: Re: [isabelle] Extra type variables in constdef
- Cl-isabelle-users October 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list