Re: [isabelle] Non-determinism
It is not clear what you mean by doing an assignment in Isabelle. I assume
you want to define a new constant without setting its actual value using
an equality. There already exists an 'arbitrary' constant in Isabelle you
can use for this :
Otherwise you can use definition by specification:
random :: nat
"random > 10 & random < 20"
Here a new constant is defined with the property that is a nat in the
Hope I was on the right track,
On Thu, 7 Sep 2006, Gabriele Pozzani wrote:
it's possible to do a non-deterministic assignment in Isabelle, or simulate
Or, it's possible generate a random integer?
Thanks in advance for the collaboration.
This archive was generated by a fusion of
Pipermail (Mailman edition) and