[isabelle-dev] NEWS: Case translations as a separate check phase independent of the datatype package

[Dmitriy Traytel]

On 24.04.2013 16:18, Brian Huffman wrote:
> On Wed, Apr 24, 2013 at 2:52 AM, Dmitriy Traytel <traytel at in.tum.de> wrote:
>> However, your example is still not printed as expected (assuming that the
>> output should be equal to the input in this case):
>>
>> "(case x of (a, b) => λ(c, d). e) y"
> Usually "prod_case" is printed as a tuple-lambda when partially
> applied, and as a case expression when fully applied. So considering
> that the underlying term in my example is "prod_case (λa b. prod_case
> (λc d. e)) x y", the above output makes perfect sense.
I see. Previously, I though that "prod_case" is always supposed to be 
printed as a lambda with a pattern and the fact that it is printed as a 
case expression sometimes is a coincidence caused by the order in which 
syntax translations are applied. But your explanation makes sense and 
results in less work for me :-)

Dmitriy