*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Continuing with a proof after a failed 'done'*From*: Lars Hupel <hupel at in.tum.de>*Date*: Tue, 2 Aug 2016 16:56:09 +0200*In-reply-to*: <be97178d-d9f6-2fac-a9de-c0a985d23545@inf.ethz.ch>*References*: <40a825f7-63b2-a21c-3116-6ace8970a1a9@in.tum.de> <02266e2a-a673-c86f-0cbe-aea189c95762@inf.ethz.ch> <99090bdd-7764-8599-58c9-32555d41df7f@in.tum.de> <be97178d-d9f6-2fac-a9de-c0a985d23545@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0

> Neither do I understand why they behave differently. Probably only > Makarius knows. The short forms "." and ".." also behave like done and > differently from their long forms "by this" and "by rule". It looks like > "by" is the outsider, because "proof(rule) qed" does not close the proof > block, either. Right, I forgot about 'qed'. This one is not as easy to work around using a single strategically placed 'sorry'.

**References**:**[isabelle] Continuing with a proof after a failed 'done'***From:*Lars Hupel

**Re: [isabelle] Continuing with a proof after a failed 'done'***From:*Andreas Lochbihler

**Re: [isabelle] Continuing with a proof after a failed 'done'***From:*Lars Hupel

**Re: [isabelle] Continuing with a proof after a failed 'done'***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Continuing with a proof after a failed 'done'
- Next by Date: Re: [isabelle] Continuing with a proof after a failed 'done'
- Previous by Thread: Re: [isabelle] Continuing with a proof after a failed 'done'
- Next by Thread: Re: [isabelle] Continuing with a proof after a failed 'done'
- Cl-isabelle-users August 2016 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