Re: [isabelle] find_consts does not find inductive sets



> 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 *)
> end
> 
> 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.

	Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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