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

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