equal
deleted
inserted
replaced
47 support for higher-order features (esp. lambda abstractions). |
47 support for higher-order features (esp. lambda abstractions). |
48 It is an incomplete decision procedure based on external SMT |
48 It is an incomplete decision procedure based on external SMT |
49 solvers using the oracle mechanism; for the SMT solver Z3, |
49 solvers using the oracle mechanism; for the SMT solver Z3, |
50 this method is proof-producing. Certificates are provided to |
50 this method is proof-producing. Certificates are provided to |
51 avoid calling the external solvers solely for re-checking proofs. |
51 avoid calling the external solvers solely for re-checking proofs. |
|
52 |
|
53 * New counterexample generator tool "nitpick" based on the Kodkod |
|
54 relational model finder. |
52 |
55 |
53 * Reorganization of number theory: |
56 * Reorganization of number theory: |
54 * former session NumberTheory now named Old_Number_Theory |
57 * former session NumberTheory now named Old_Number_Theory |
55 * new session Number_Theory by Jeremy Avigad; if possible, prefer this. |
58 * new session Number_Theory by Jeremy Avigad; if possible, prefer this. |
56 * moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/; |
59 * moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/; |