[isabelle-dev] [isabelle] Error: Non-constructor pattern not allowed in sequential mode

[Makarius]

On Tue, 5 Jul 2011, Tobias Nipkow wrote:

> I agree with Gerwin. Records are datatypes. Hence one should be able to 
> pattern match against them as in FP languages.

See also 
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2006-December/msg00000.html
as an arbitrary point in the really long history of these highly complex 
packages.


> The record package can arrange for this very easily via rep_datatype.

No.  It will involve much more things that were not even touched in the 
discussion yet.


 	Makarius