Re: [isabelle] The "inductive" command loops



Hi Joachmim,

> the declaration
> 
>         inductive foo :: "int â bool" where "P x â foo x" -- "note the free P!"
>         
> makes the system loop during "Proving the simplification rules ...".

thanks for your report.  According to your description, the computation
of the inductive.simps seems to be faulty.  Is anybody out there who can
investigate this?

All the best,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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