[isabelle-dev] simplifier trace (and jedit)

[Makarius]

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.


 	Makarius