Re: [isabelle-dev] [isabelle] print_statement does not quote variables with reserved names

2016-10-28 Thread Andreas Lochbihler

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).


Andreas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] [isabelle] print_statement does not quote variables with reserved names

2016-10-28 Thread Makarius
On 28/10/16 13:52, Lawrence Paulson wrote:
> I hope these won't be deprecated. Even though they are a bit longer, they are 
> logical and easy to remember (due to the parallels with fix/assume/show).
> Larry
> 
>> On 27 Oct 2016, at 22:20, Makarius  wrote:
>>
>> Note that the long form with fixes/assumes/shows has become a bit
>> old-fashioned, although there is nothing wrong with it apart from being
>> too long for short statements.
>>
>> The new eigen-context notation "theorem B if A for x" often works
>> better, but there no print command for that yet. In fact, I would like
>> to make the "for x" form standard for almost all output, e.g. plain
>> 'thm'. But that is a different story for a different release.
> 

fixes/assumes/show is not going to disappear; it is required as dual
form of fixes/assumes/obtains, which is not covered by the new
eigen-context notation.

BTW, there is strictly speaking no need to use fix/assume/show, since
show if/for is already possible, although relatively rarely used.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev