Re: [isabelle] automatic case splitting during simp



Allow me to send an immediate bugfix. I thought I was being clever by replacing HOL conjunction with Pure conjunction in the output of split_simps, but it appears that the simplifier doesn't know what to do with it.

Redefining conjunct_rules like this fixes it:
val conjunct_rules = foldr1 (fn (a, b) => [a, b] MRS conjI);

The reason for this is that theorem-modifying attributes don't seem to be able to emit a list of theorems, so I had to fold the theorems back into a single one. Perhaps the isabelle developers can think of a better way.

I attach the newest version.

Yours,
    Thomas.

Attachment: SplitSimps.thy
Description: SplitSimps.thy



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