[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 *)
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and