[isabelle-dev] [isabelle] print_statement does not quote variables with reserved names
andreas.lochbihler at inf.ethz.ch
Fri Oct 28 17:51:16 CEST 2016
On 28/10/16 17:03, Makarius wrote:
> BTW, there is strictly speaking no need to use fix/assume/show, since
> show if/for is already possible, although relatively rarely used.
I use show/if/for regularly in my work (just look at the AFP entry MFMC_Countable to see a
few examples), but fix/assume/show is more convenient if the proof needs intermediate
"have" steps between the "assume" and the "show". The show/if/for pattern is possible in
this case, but I'd have to open another "proof - have ... show ?thesis ... qed" block,
which introduces clutter and unnecessary indentation.
Also, if there are several goals with the same assumptions, fix/assume/show/show/show/...
is more concise than having to repeat the assumptions for every show (if each goal needs a
different proof method invocation).
More information about the isabelle-dev