[isabelle] Apply rule: unexpected behaviour



I am working with a theory where the application of certain rule fails when
placed in the middle of a larger proof, but if I declare a new theorem
containing exactly the problematic sub goal (where the application fails),
then Isabelle allows me to apply the rule I want in the proof of the new
theorem.

Originally, I suspected this was caused by some type mismatch, and I
enabled types in the output to investigate if the types match. They do. I
didn't find anything that makes the goal in the larger proof different from
its copied and pasted version used to create a new theorem.

Is there any way of extracting more information from Isabelle about the
reason that causes the application of a rule to fail?


Thanks,

Diego



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