[isabelle] find_consts does not find constants from BNF package

Dear BNF developers,

I noticed that find_consts does not find the constants for the set and map functions and the relator. For _ list, for example, none of the following commands find the functions defined by the datatype declaration in List.thy (in Isabelle2015):

find_consts "(_ â _) â _ list â _ list" (* map not found *)
find_consts "(_ â _ â bool) â _ list â _ list â bool" (* list_all2 not found *)
find_consts "_ list â _ set" (* set not found *)

Could this be changed such that find_consts can find them? I was puzzled today in our Isabelle course when I wanted to search for map and find_consts simply did not show it.


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