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

[Florian Haftmann]

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

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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