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