[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
How can I do? The only way is to define a recursive function?
Thanks in advance,
This archive was generated by a fusion of
Pipermail (Mailman edition) and