Re: [isabelle] Apply rule: unexpected behaviour

Hi Lars,

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
find out
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> 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.
> Cheers
> Lars

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