Am 04/04/2012 11:48, schrieb Tjark Weber: > Adhering to the principle of least astonishment, I suspect an error > message (or at least a warning) would be more helpful.
Isabelle's well-tried principle of least astonishment is not to give too many helpful error messages or warnings ;-) Actually, in this case it is not so easy to produce an error message because the patterns are translated away with translations and the resulting lambda's are perfectly legal. Tobias _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
