[isabelle-dev] [isabelle] Error: Non-constructor pattern not allowed in sequential mode
makarius at sketis.net
Wed Jul 6 11:09:49 CEST 2011
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.
as an arbitrary point in the really long history of these highly complex
> 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
More information about the isabelle-dev