[isabelle-dev] "rep_datatype" is illegal in local theory mode

Christian Sternagel c-sterna at jaist.ac.jp
Thu Jun 7 05:01:48 CEST 2012

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?



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

More information about the isabelle-dev mailing list