[isabelle-dev] Pattern matching on finite trees [was: "rep_datatype" is illegal in local theory mode]
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?
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev