[isabelle-dev] Pattern matching on finite trees [was: "rep_datatype" is illegal in local theory mode]

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Jun 15 20:51:34 CEST 2012

> 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"?

Hmmmm... have you got specification pieces which illustrate what you
want to accomplish more exactly?



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120615/51305e29/attachment.sig>

More information about the isabelle-dev mailing list