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.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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