[isabelle-dev] case syntax

[Makarius]

On Wed, 11 Jan 2012, Alexander Krauss wrote:

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

Just to illuminate the general situation a bit, can you point to relevant 
parts of your thesis, also the one of Konrad Slind for the old version? 
Stefan had mentioned that at some point "as everybody knows, Konrad used 
to do it like that" without giving a reference.


 	Makarius