[isabelle] Bug in Sledgehammer / cvc4



When I tried sledgehammer on the following theorem:

theorem Max_ge': "finite A â x > Max A â Â(x â A)"

The cvc4 output is:
Try this: using leD by auto (6 ms).

However, the command does not work. It probably should be
using Max_ge leD by auto

Best,
Bohua




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