Re: [isabelle] Modelcheck example
On Mon, 4 Sep 2006, Gabriele Pozzani wrote:
> I proved to use the examples about the integration between Isabelle and
> Mucke. I have installed Isabelle 2005 and Mucke 0.4.4.
> Isabelle analyse theory MuckeExample1 (in HOL/Modelcheck) but when it
> reaches lemma "reach_ex1" and in particular the application of the second
> tactic it stops with the follow error:
Unfortunately, the Mucke interface has not been used for a long time.
These files are essentially the leftover of some experiments with Mucke
0.3.5 -- according to the README. Both Isabelle and Mucke may well have
changed to make this kind of oracle code break down.
This archive was generated by a fusion of
Pipermail (Mailman edition) and