[isabelle-dev] case syntax
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