[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution

[Makarius]

On Tue, 8 Feb 2011, Brian Huffman wrote:

> * Instantiating a rule proved within an open-brace-close-brace block
> in a structured proof. I was surprised by this one. For example:
>
> lemma "True"
> proof -
>  { fix n :: nat
>    have "n = n" by simp
>  }
>
> this:
>  ?n2 = ?n2
>
> I expected "this" to have the form "?n = ?n", with index 0. But for some 
> reason, the actual rule uses index 2. Some proof scripts in SEQ.thy use 
> something like "note foo = this", followed later with an instantiation 
> using the "where" attribute that refers to the nonzero index.

Continuing your experiments maybe a few more months, you will discover 
more details.

Back in the mid 1990-ies, one could still consider changing the system 
from a quick impulse to try a variation of existing functionality.  Later 
this has become much more tedious, and now its an arcane discipline.


 	Makarius