*To*: noam neer <noamneer at gmail.com>*Subject*: Re: [isabelle] some problems with the /\ quantifier*From*: Larry Paulson <lp15 at cam.ac.uk>*Date*: Sun, 13 Sep 2015 10:47:53 +0100*Cc*: Lars Hupel <hupel at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAGOKs0_YyEvN39x-UXL6jnofDj-A2pfo35qsGxn6KSNCBKwUjA@mail.gmail.com>*References*: <CAGOKs09PRLE1E97Sw9ri493tdjA8G3vRMAMYyWm+TBf0nfxVuA@mail.gmail.com> <55F50825.9020104@in.tum.de> <CAGOKs0_YyEvN39x-UXL6jnofDj-A2pfo35qsGxn6KSNCBKwUjA@mail.gmail.com>

> your recommended solution uses 'auto' which I try not to use too much because > I'm not sure what exactly it is doing, and I prefer simple commands like > [of ...] or 'rule_tac' for this reason. I guess this is also a kind of > robustness consideration. I know that others share such views, and they make sense on occasion, above all when you are trying to figure out how logic works. But itâs not a practical attitude if you want to get much work done. Assuming that you are using structured proofs, auto does not harm robustness; on the contrary, it can be more robust than single-step proofs, which often break in the presence of the slightest change. How much work will you have to do if you find yourself changing a definition? Larry Paulson

**References**:**[isabelle] some problems with the /\ quantifier***From:*noam neer

**Re: [isabelle] some problems with the /\ quantifier***From:*Lars Hupel

**Re: [isabelle] some problems with the /\ quantifier***From:*noam neer

- Previous by Date: Re: [isabelle] some problems with the /\ quantifier
- Next by Date: [isabelle] We are looking for Proof Engineers!
- Previous by Thread: Re: [isabelle] some problems with the /\ quantifier
- Next by Thread: [isabelle] We are looking for Proof Engineers!
- Cl-isabelle-users September 2015 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