[isabelle] The "inductive" command loops



Hi,

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?

Thanks,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

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



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