[isabelle-dev] Redundant equations in function declarations

[Makarius]

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