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.


	Makarius





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