[isabelle-dev] simplifier trace (and jedit)
makarius at sketis.net
Thu May 31 13:53:54 CEST 2012
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.
More information about the isabelle-dev