[isabelle] The "inductive" command loops


the declaration

        inductive foo :: "int â bool" where "P x â foo x" -- "note the free P!"
makes the system loop during "Proving the simplification rules ...".
Such an inductive predicate is probably not very useful, but it maybe it
is still possible to make "inductive" a mit more robust in this respect?


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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