equal
deleted
inserted
replaced
78 Minor INCOMPATIBILITY. |
78 Minor INCOMPATIBILITY. |
79 |
79 |
80 * Session HOL-Word: Operations lsb, msb and set_bit are separated |
80 * Session HOL-Word: Operations lsb, msb and set_bit are separated |
81 into theories Misc_lsb, Misc_msb and Misc_set_bit respectively. |
81 into theories Misc_lsb, Misc_msb and Misc_set_bit respectively. |
82 INCOMPATIBILITY. |
82 INCOMPATIBILITY. |
|
83 |
|
84 * Session HOL-TPTP: The "tptp_isabelle" and "tptp_sledgehammer" |
|
85 commands are in working order again, as opposed to outputting |
|
86 "GaveUp" on nearly all problems. |
83 |
87 |
84 * Simproc defined_all and rewrite rule subst_all perform |
88 * Simproc defined_all and rewrite rule subst_all perform |
85 more aggressive substitution with variables from assumptions. |
89 more aggressive substitution with variables from assumptions. |
86 INCOMPATIBILITY, use something like |
90 INCOMPATIBILITY, use something like |
87 "supply subst_all [simp del] [[simproc del: defined_all]]" |
91 "supply subst_all [simp del] [[simproc del: defined_all]]" |