Re: [isabelle] Apply rule: unexpected behaviour
The clash information I get is this: "Lattices.sup_class.sup =/=
It understood that it has to do with the usage of sets, but I will need to
how this message can help me. Does this clash message ring a bell for you?
Thanks for you help!
On 13 March 2016 at 18:59, Lars Hupel <hupel at in.tum.de> wrote:
> Hi Diego,
> > Is there any way of extracting more information from Isabelle about the
> > reason that causes the application of a rule to fail?
> try this:
> using [[unify_trace_failure]]
> apply (rule ...)
> Then, you'll find the output like the following:
> Clash: Scratch.P =/= Scratch.Q
> Hope that helps.
This archive was generated by a fusion of
Pipermail (Mailman edition) and