equal
deleted
inserted
replaced
75 Minor INCOMPATIBILITY. |
75 Minor INCOMPATIBILITY. |
76 |
76 |
77 * Session HOL-Word: Theory Z2 is not used any longer. |
77 * Session HOL-Word: Theory Z2 is not used any longer. |
78 Minor INCOMPATIBILITY. |
78 Minor INCOMPATIBILITY. |
79 |
79 |
80 * Rewrite rule subst_all performs |
80 * Simproc defined_all and rewrite rule subst_all perform |
81 more aggressive substitution with variables from assumptions. |
81 more aggressive substitution with variables from assumptions. |
82 INCOMPATIBILITY, use something like |
82 INCOMPATIBILITY, use something like |
83 "supply subst_all [simp del]" |
83 "supply subst_all [simp del] [[simproc del: defined_all]]" |
84 to leave fragile proofs unaffected. |
84 to leave fragile proofs unaffected. |
85 |
85 |
86 |
86 |
87 *** FOL *** |
87 *** FOL *** |
88 |
88 |