*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Isar syntax question*From*: Joachim Breitner <breitner at kit.edu>*Date*: Thu, 17 Jul 2014 10:54:25 +0200*In-reply-to*: <2FBE95AA-17AD-4DA1-AB09-6766B79B4B37@cmu.edu>*References*: <2FBE95AA-17AD-4DA1-AB09-6766B79B4B37@cmu.edu>

Hi, Am Mittwoch, den 16.07.2014, 15:00 -0700 schrieb Vadim Zaliva: > I am learning Isar and have another naive question on the syntax: > I am trying to do something like this in Isar: > > 1: lemma > 2: shows "not something" > 3: proof(rule ccontr) > 4: assume "something" > 5: thus False proof cases > 6: ... > 7: qed > 8: qed > > and get "*** Failed to refine any pending goal" error around line 5 > > Why this does not work? Something like this works instead: > > lemma > shows "not something" > proof > assume "something" > hence False proof cases > ... > qed > thus False by simp > qed it would be very helpful, especially for beginners, but often also for me, if a "proof" would tell us what rule it applied – similar to how "also" tells us what the current calculation is. (And while are are at it: "also" could also tell us what rule it used...) Such features give great insight into the system and give the users more confidence in using it. Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Isar syntax question***From:*Makarius

**References**:**[isabelle] Isar syntax question***From:*Vadim Zaliva

- Previous by Date: Re: [isabelle] Record for module?
- Next by Date: Re: [isabelle] Isar syntax question
- Previous by Thread: Re: [isabelle] Isar syntax question
- Next by Thread: Re: [isabelle] Isar syntax question
- Cl-isabelle-users July 2014 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