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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
