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
*** Isar ***
* Proof methods may refer to the main facts via the dynamic fact
"method_facts". This is particularly useful for Eisbach method
definitions.
* Eisbach provides method "use" to modify the main facts of a given
method expression, e.g.
(use facts in simp)
(use facts in ‹simp add: