Re: [isabelle] Apply rule: unexpected behaviour



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.