Re: [isabelle] find_consts does not find constants from BNF package

Hi Andreas,

thanks for the report. (The BNF constants were concealed for almost two years now, without anyone noticing!)

It should be better with the repository version isabelle/69a97fc33f7a.


On 22.09.2015 17:07, Andreas Lochbihler wrote:
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.