|
|
|
|
|
|
by logicchains
2337 days ago
|
|
|
They have not been solved. My point was that automation via Coq's tactic language can serve as a decent substitute for "push-button" automation like Hammers, at least if one's continually working in the same domain and so can build up a library of tactics. |
|
|