equal
deleted
inserted
replaced
45 |
45 |
46 * Renamed theorems: |
46 * Renamed theorems: |
47 Suc_eq_add_numeral_1 -> Suc_eq_plus1 |
47 Suc_eq_add_numeral_1 -> Suc_eq_plus1 |
48 Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left |
48 Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left |
49 Suc_plus1 -> Suc_eq_plus1 |
49 Suc_plus1 -> Suc_eq_plus1 |
|
50 |
|
51 * New sledgehammer option "Full Types" in Proof General settings menu. |
|
52 Causes full type information to be output to the ATPs. This slows ATPs down |
|
53 considerably but eliminates a source of unsound "proofs" that fail later. |
50 |
54 |
51 * Discontinued ancient tradition to suffix certain ML module names with "_package", e.g.: |
55 * Discontinued ancient tradition to suffix certain ML module names with "_package", e.g.: |
52 |
56 |
53 DatatypePackage ~> Datatype |
57 DatatypePackage ~> Datatype |
54 InductivePackage ~> Inductive |
58 InductivePackage ~> Inductive |