Hi all,
I am just curious whether the reason for rep_datatype being illegal in
local theory mode is that the datatype package is not fully localized
yet (in which case it is conceivable that this will work some day, which
would be nice) or that this is inherently not possible to realize?
cheers
chris
PS: I am just playing around with a locale for finite trees and wanted
to introduce some recursive functions (and later also inductive
predicates) but pattern matching is only possible on constructors. Is
anybody aware of an earlier attempt for doing such a thing or a better
way to prove something "for all kinds of (non empty) finite trees"?
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
