On 09/06/16 16:25, Joachim Breitner wrote:
>
> But while I like "using" inside an proof, it does not please my sense
> of aesthetic to have such a command before the initial "proof" command.
Such initial 'using' is sometimes indeed awkward, but there is in
general nothing wrong with it.
BTW,
Dear Markarius,
Am Donnerstag, den 09.06.2016, 15:58 +0200 schrieb Makarius:
>
> [..] Turning 'using' into "use" is a downgrade of proof command into proof
> method. This is occasionally useful, like e.g. using attribute
> expressions instead of proof methods, but not something I would do all
>
Hi,
Am Mittwoch, den 08.06.2016, 19:46 +0200 schrieb Makarius:
> There are further possibilities for "use", e.g. to eliminate
> auxiliary
> "-" or "insert" steps, notably:
>
> qed (insert a, auto) ~> qed (use a in auto)
does this mean that the old idiom of
lemma foo:
assumes
