[isabelle-dev] case syntax

[Alexander Krauss]

On 01/11/2012 06:18 PM, Makarius wrote:
> As I've discussed this with Stefan and Brian already in december. The
> idea is to separate superficial case syntax translations from the main
> work in a suitable check/unckeck phase. E.g. certain packages could
> provide abstract syntax (like abbreviations) for destructors, and issue
> a suitable context declaration to relate groups of them with certain
> case combinators.

This would be a big improvement to this code.

One rather old thing on my list is to move the function package back to 
using the same transformation (an older version of the same code is part 
of TFL), since my ad-hoc translation 
(HOL/Tools/Function/pattern_split.ML) is ocasionally more problematic, 
and I would prefer to keep things uniform. Having a decent check/uncheck 
phase with fully typed terms would probably make this a bit less unpleasant.


Alex