Re: [isabelle] find_consts does not find inductive sets

Hi Florian,

Thanks for addressing this.


On 22/09/15 16:13, Florian Haftmann wrote:
I noticed that find_consts does not find constants defined with
inductive_set. Here is a minimal example (for Isabelle2015):

theory Scratch imports Main begin
inductive_set foo :: "nat set => bool set" for x where "a : foo x"
find_consts "nat set => bool set" (* returns nothing *)
find_consts "nat set => bool => bool" (* returns foop *)

I think this should be changed such that inductively defined sets can
also be found---unless someone can convince me that the current
behaviour is desirable.

See now 61908914d191 and c94c65f35d01.



PGP available:

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