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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
