[isabelle-dev] case syntax
krauss at in.tum.de
Wed Jan 11 20:44:49 CET 2012
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.
More information about the isabelle-dev