equal
deleted
inserted
replaced
230 less_eq_multiset_def |
230 less_eq_multiset_def |
231 INCOMPATIBILITY |
231 INCOMPATIBILITY |
232 |
232 |
233 * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef' |
233 * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef' |
234 command. Minor INCOMPATIBILITY, use 'function' instead. |
234 command. Minor INCOMPATIBILITY, use 'function' instead. |
|
235 |
|
236 |
|
237 ** ML ** |
|
238 |
|
239 * Thm.instantiate (and derivatives) no longer require the LHS of the |
|
240 instantiation to be certified: plain variables are given directly. |
235 |
241 |
236 |
242 |
237 |
243 |
238 New in Isabelle2015 (May 2015) |
244 New in Isabelle2015 (May 2015) |
239 ------------------------------ |
245 ------------------------------ |