*To*: Gabriele Pozzani <gabriele.pozzani at gmail.com>*Subject*: Re: [isabelle] Create automaton in a function*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 04 Oct 2006 11:01:34 +0200*Cc*: Isabelle <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <b3262abf0610030256qc54a72ckecb6c1475f8ce7b8@mail.gmail.com>*References*: <b3262abf0610030256qc54a72ckecb6c1475f8ce7b8@mail.gmail.com>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

Tobias Gabriele Pozzani wrote:

Hello, I have created an I/O automaton using the Isabelle syntax in HOLCF/IOA. Now I have a problem. Can I create an automaton in a function? What I want is something like this: defs fdef: "f a == automaton auto = signature actions "enne action" ...." but the problem is that the definition of the function require a string, but when I insert the function body between two " Isabelle give me a syntax error. I tried to use the escape sequence for " that is \" but Isabelle return a lexical error in the definition of the states. There is another way to do that? Thanks Gabriele

**References**:**[isabelle] Create automaton in a function***From:*Gabriele Pozzani

- Previous by Date: Re: [isabelle] Isabelle + NuSMV
- Next by Date: Re: [isabelle] List construction
- Previous by Thread: [isabelle] Create automaton in a function
- Next by Thread: [isabelle] List construction
- Cl-isabelle-users October 2006 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