Re: [isabelle] rule Unifies With Chained Facts?

On Sat, 2 Apr 2011, Brian Huffman wrote:

It is a bit confusing how "rule" treats chained facts in a special way, when nearly all other methods start by adding any chained facts into the goal as premises before continuing with their normal behavior. It is also a bit inconvenient that there is no single method that has the "insert chained facts, then apply a rule" behavior; but at least there is an easy workaround with "-" followed by "rule".

The treatment of chained facts by "rule" is inherent in the way how Isar really works. Part of the confusion stems from the very liberal language design which also admits many "improper" elements in the same language.

If you really want to understand structure Isar proofs, not proof scripts, you need to become acquainted with Isar rule composition.


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