[isabelle] Create automaton in a function



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




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