*To*: Yevgeniy Makarov <emakarov at gmail.com>*Subject*: Re: [isabelle] Questios about evaluation and code extraction*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sat, 13 Jan 2007 10:12:52 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <68e6491b0701120224j399eee3dh6a6c6b61ef11f320@mail.gmail.com>*References*: <68e6491b0701120224j399eee3dh6a6c6b61ef11f320@mail.gmail.com>*User-agent*: Thunderbird 1.5.0.2 (Macintosh/20060308)

(1) Is it possible to evaluate, or normalize, terms inside Isabelle? I know that one can exract executable specifications to ML ("Isabelle's Logics: HOL", Section 2.9). I also know that in the proof mode I can say apply(simp) to simplify, say, the goal "(12 :: int) div 5 = 2" to True. But can I make Isabelle compute the result of "(12 :: int) div 5"?

Try the Isar command value "...."

(2) Is it possible to extract code from fragments that use rational numbers? When I tried the following code:

Tobias

**References**:**[isabelle] Questios about evaluation and code extraction***From:*Yevgeniy Makarov

- Previous by Date: Re: [isabelle] trivial proof to solve/reply
- Next by Date: [isabelle] bug in application of intro rule for SOME P when its type is a function?
- Previous by Thread: [isabelle] Questios about evaluation and code extraction
- Next by Thread: [isabelle] bug in application of intro rule for SOME P when its type is a function?
- Cl-isabelle-users January 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