equal
deleted
inserted
replaced
246 INCOMPATIBILITY, need to provide explicit type constraints for Pure |
246 INCOMPATIBILITY, need to provide explicit type constraints for Pure |
247 types where this is really intended. |
247 types where this is really intended. |
248 |
248 |
249 |
249 |
250 *** HOL *** |
250 *** HOL *** |
|
251 |
|
252 * Dedicated syntax LENGTH('a) for length of types. |
251 |
253 |
252 * New proof method "argo" using the built-in Argo solver based on SMT |
254 * New proof method "argo" using the built-in Argo solver based on SMT |
253 technology. The method can be used to prove goals of quantifier-free |
255 technology. The method can be used to prove goals of quantifier-free |
254 propositional logic, goals based on a combination of quantifier-free |
256 propositional logic, goals based on a combination of quantifier-free |
255 propositional logic with equality, and goals based on a combination of |
257 propositional logic with equality, and goals based on a combination of |