[isabelle-dev] Redundant equations in function declarations

Makarius makarius at sketis.net
Tue May 29 17:44:51 CEST 2012


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



More information about the isabelle-dev mailing list