equal
deleted
inserted
replaced
15 * On instantiation of classes, remaining undefined class parameters |
15 * On instantiation of classes, remaining undefined class parameters |
16 are formally declared. INCOMPATIBILITY. |
16 are formally declared. INCOMPATIBILITY. |
17 |
17 |
18 |
18 |
19 *** HOL *** |
19 *** HOL *** |
|
20 |
|
21 * New proof method "smt" for a combination of first-order logic |
|
22 with equality, linear and nonlinear (natural/integer/real) |
|
23 arithmetic, and fixed-size bitvectors; there is also basic |
|
24 support for higher-order features (esp. lambda abstractions). |
|
25 It is an incomplete decision procedure based on external SMT |
|
26 solvers using the oracle mechanism. |
20 |
27 |
21 * Reorganization of number theory: |
28 * Reorganization of number theory: |
22 * former session NumberTheory now named Old_Number_Theory |
29 * former session NumberTheory now named Old_Number_Theory |
23 * new session Number_Theory by Jeremy Avigad; if possible, prefer this. |
30 * new session Number_Theory by Jeremy Avigad; if possible, prefer this. |
24 * moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/; |
31 * moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/; |