On Tue, 29 May 2012, Lawrence Paulson wrote:
I'm not talking about user interfaces or models. I am saying that
function definitions containing entirely redundant equations should be
rejected, also in batch mode.
Maybe you can do some routine investigations why the current situation
(63021e59cbf0) of the function package is the way it is.
One has to make a proof against the overwhelming Isabelle history, before
speculating what is right or wrong.
Moreover one needs to hear what the experts say (probably Alex Krauss,
Stefan Berghofer, Lukas Bulwahn).
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
