[isabelle] Inductive Set Definitions

Morning all, I have been away from Isabelle for a long time. Now I need to define inductively a function that takes a set and returns a set of sets, built inductively starting from the input one.

In the previous versions of Isabelle i used the "induct" construct to do that, but with the later version its counterpart "induct_set" does not allow this.

How can I do? The only way is to define a recursive function?

Thanks in advance,
Cristiano Longo

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