*To*: Yannick <yannick_duchene at yahoo.fr>*Subject*: Re: [isabelle] Isabelle2013-RC2 available for testing*From*: Makarius <makarius at sketis.net>*Date*: Wed, 6 Feb 2013 22:31:23 +0100 (CET)*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <op.wr3qv2a2esn74s@cardamome>*References*: <alpine.LNX.2.00.1301281758520.25806@macbroy21.informatik.tu-muenchen.de> <op.wr13h2bjule2fv@cardamome> <op.wr16v3mdule2fv@cardamome> <alpine.LNX.2.00.1302061645280.24399@macbroy21.informatik.tu-muenchen.de> <op.wr3j13e5esn74s@cardamome> <alpine.LNX.2.00.1302062004560.20498@macbroy21.informatik.tu-muenchen.de> <op.wr3pysihesn74s@cardamome> <alpine.LNX.2.00.1302062137400.7597@macbroy21.informatik.tu-muenchen.de> <op.wr3qv2a2esn74s@cardamome>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Wed, 6 Feb 2013, Yannick wrote:

Note that method "rule" is dynamically rebound in HOL to include rules stemming from the classical reasoner, too. Cf. print_claset.I'm not sure to understand what it implies, but will learn“print_claset”, as you mention it.

Before I came to Isabelle, at the time I didn't knew any prover system,I tried to imagine such things, and in my mind, this was always comingwith this: “if it automate some proof or proof step, the user should beable to learn what the steps was, it should be visible in some way”.That's important, as the matter, I feel, is not only about the proverunderstanding a proof, but also about the human author and human reader,understanding it too.

notepad begin note [[rule_trace]] have "A ∧ B" proof -- trace show A sorry show B sorry qed from `A ∧ B` obtain A and B ..-- trace end

Makarius

**Follow-Ups**:**Re: [isabelle] Isabelle2013-RC2 available for testing***From:*Gottfried Barrow

**References**:**Re: [isabelle] Isabelle2013-RC2 available for testing***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Isabelle2013-RC2 available for testing***From:*Yannick Duchêne (Hibou57)

**Re: [isabelle] Isabelle2013-RC2 available for testing***From:*Makarius

**Re: [isabelle] Isabelle2013-RC2 available for testing***From:*Yannick

**Re: [isabelle] Isabelle2013-RC2 available for testing***From:*Makarius

**Re: [isabelle] Isabelle2013-RC2 available for testing***From:*Yannick

- Previous by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- Next by Date: Re: [isabelle] Isabelle2013-RC2 available for testing
- Previous by Thread: Re: [isabelle] Isabelle2013-RC2 available for testing
- Next by Thread: Re: [isabelle] Isabelle2013-RC2 available for testing
- Cl-isabelle-users February 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list