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
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,
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.,
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.
Dear all,
I wanted to write this already a long time ago (prompted by an Isabelle
course I gave) but somehow forgot about it. Now I had a look at my
slides again and was reminded.
1) The first thing is rather subjective, but maybe you could comment on
it. I think the simplifier trace would
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
