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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
