Re: [isabelle] apply simp: Tactic failed



> A quick look into the simpset reveals that the simproc
> 'list_to_set_comprehension' is likely at fault. Indeed, after disabling
> it, 'simp' goes through (doesn't solve the goal, though). Apparently the
> simproc internally sets up some goal via 'Goal.prove' which it cannot solve.

This seems (again) an indication, that either somebody invests some time
to restore that simproc, or make it optional alternatively.

	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.