*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Date*: Tue, 09 Feb 2010 00:09:07 +1100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4B700AB7.4040101@informatik.tu-muenchen.de>*References*: <4B6F1CA6.3080906@cse.unsw.edu.au> <4B6FE929.8060809@informatik.tu-muenchen.de> <4B7009A5.7030303@cse.unsw.edu.au> <4B700AB7.4040101@informatik.tu-muenchen.de>*User-agent*: Thunderbird 2.0.0.23 (X11/20090817)

Florian Haftmann wrote:

The "prems" are, roughly, the accumulated facts within a proof, which as a historical accident have been used implicitly by certain proof methods -- which, following the rule of thumb "explicit is better than implicit", turned out as a bad idea. You can recover this behaviour by using prems explicitly, e.g. "using prems by ..." or "by (auto simp add: prems)" etc. Best practice is to refer to used facts implicitly; recall that you can quote facts by proposition using backticks ``.

Does this mean I should be writing: next case (Cons x xs) from prems have ... instead of next case (Cons x xs) hence ... ? Sincerely, Rafal Kolanski.

**Follow-Ups**:**Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?***From:*Florian Haftmann

**References**:**[isabelle] More use of "-" and "!" in isabelle 2009-1?***From:*Rafal Kolanski

**Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?***From:*Florian Haftmann

**Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?***From:*Rafal Kolanski

**Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?
- Next by Date: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?
- Previous by Thread: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?
- Next by Thread: Re: [isabelle] More use of "-" and "!" in isabelle 2009-1?
- Cl-isabelle-users February 2010 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