[isabelle] find_theorems and locales
find_theorems doesn't seem to find locale definitions. Is this behavior
intentional? For example:
locale xyzzy = assumes "Some () = None"
(* xyzzy ?P == ?P *)
(* 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.
PS. versions: Isabelle 2014, Isabelle 2015, eb3094c6576c
This archive was generated by a fusion of
Pipermail (Mailman edition) and