On Wed, 23 May 2012, Thomas Sewell wrote:

The _2 v.s. (2) thing is just silly. It's in find_theorems output too.

This was changed many years ago, i.e. find_theorems already uses correct fact references in terms of the user context, e.g. foo(2) for fact foo.

The internal derivation name foo_2 (or "name hint", these things are not so well defined) sometimes occurs as a fall-back in tools that only have derivatations available not the facts environment. Things like 'unused_thms' come to mind.

It's just the way theorems get their names - probably one of these decisions made years ago and not compatible with Makarius' decisions about how to fetch theorems in Isar.

"Decisions" often mean one does not know any better than tossing a coin. It is better to conclude good things from the given assumptions of what is there already, or a slight reform of it.

Historically, there is the odd situation that I introduced the foo_2 naming scheme for internal derivations, and Stefan Berghofer the foo(2) syntax for Isar fact references. Then we tried hard for many years to get rid of foo_2 for most user situations, but did not fully succeed yet.

isabelle-dev mailing list

Reply via email to