Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-25 Thread Makarius
On Thu, 24 May 2012, Christian Sternagel wrote: The Prover Session panel has check/cancel buttons that are reminiscent of manual control in PG. The keyboard shortcuts are C-SPACE and C-BACKSPACE, respectively. You need to avoid rash movements after cancelation, outerwise the checking process

Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-23 Thread Tobias Nipkow
Am 23/05/2012 06:15, schrieb Christian Sternagel: - in the [1]Rewriting: messages, we actually just see the redex and the contractum, but not the context of a rewrite step. Why not show the whole terms? (One reason against this is the high redundancy and potentially huge size of such traces,

Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-23 Thread Makarius
On Wed, 23 May 2012, Christian Sternagel wrote: 3) Furthermore, in my course I recommend students (which know about term rewriting before) to have a look at the simplifier trace whenever the simplifier does something unexpected or does not terminate. However, for the latter use-case (i.e.,

Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-23 Thread Christian Sternagel
On 05/23/2012 10:38 PM, Makarius wrote: On Wed, 23 May 2012, Christian Sternagel wrote: 3) Furthermore, in my course I recommend students (which know about term rewriting before) to have a look at the simplifier trace whenever the simplifier does something unexpected or does not terminate.

Re: [isabelle-dev] simplifier trace (and jedit)

2012-05-22 Thread Thomas Sewell
The _2 v.s. (2) thing is just silly. It's in find_theorems output too. 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. Adding context information to every reduction