[isabelle] find_theorems and locales



Hi,

find_theorems doesn't seem to find locale definitions. Is this behavior
intentional? For example:

locale xyzzy = assumes "Some () = None"

thm "xyzzy_def"
(* xyzzy ?P == ?P *)

find_theorems name:xyzzy_def
(* find_theorems name: "xyzzy_def" found nothing *)

find_theorems "Some () = None"
(* find_theorems "Some () = None" found nothing *)


This also affects completion and the Query panel in Isabelle/Jedit.

Cheers,

Bertram

PS. versions: Isabelle 2014, Isabelle 2015, eb3094c6576c




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