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, the official indendation is as follows, to emphasize that it
belongs to the proof and not the statement, thus it is at least mentally
folded away:
lemma statement
using facts (*indent +2*)
by method (*indent =2*)
lemma statement
using facts (*indent +2*)
proof (*indent -2*)
...
qed
An old-fashioned form to avoid used facts for induction works via Pure
rule statements:
lemma "x : ind_set ==> P x"
proof (induct x set: ind_set)
...
qed
> Maybe a way out would be to take inspiration of how we can avoid some
> explicit fact chaining inside proof..qed blocks, namely using "thus"
> instead of "then show"
'hence' and 'thus' are definitely obsolete: these left-over aliases from
1999, when separate 'then' did not exist. It would be better to remove
'hence' and 'thus', but it will inevitable provoke fierce complaints.
Newer commands like 'obtain' (from 2000) or 'consider' (from 2015) do
not have such a compound form.
Such aliases tend to cause bad English and confusion: just compare Isar
and Mizar in that respect, and try to explain the result to anybody out
there.
Makarius
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
