Re: [isabelle] find_theorems and locales



On 11.06.2015 11:05, Bertram Felgenhauer via Cl-isabelle-users wrote:
> Hi,
>
> find_theorems doesn't seem to find locale definitions. Is this behavior
> intentional? For example:
>
> locale xyzzy = assumes "Some () = None"

The reasoning seems to be that the locale predicate (and hence its
definition) is more or less an implementation detail of locales, so you
shouldn't access it directly. The similarly, the lemmas establishing
locale relationships are hidden from the public view. This also effects
sledgehammer.

  -- Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.