[isabelle-dev] case syntax

Makarius makarius at sketis.net
Thu Jan 12 15:33:08 CET 2012

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.


More information about the isabelle-dev mailing list