equal
deleted
inserted
replaced
244 |
244 |
245 ** ML ** |
245 ** ML ** |
246 |
246 |
247 * Thm.instantiate (and derivatives) no longer require the LHS of the |
247 * Thm.instantiate (and derivatives) no longer require the LHS of the |
248 instantiation to be certified: plain variables are given directly. |
248 instantiation to be certified: plain variables are given directly. |
|
249 |
|
250 * Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous |
|
251 quasi-bound variables (like the Simplifier), instead of accidentally |
|
252 named local fixes. This has the potential to improve stability of proof |
|
253 tools, but can also cause INCOMPATIBILITY for tools that don't observe |
|
254 the proof context discipline. |
249 |
255 |
250 |
256 |
251 |
257 |
252 New in Isabelle2015 (May 2015) |
258 New in Isabelle2015 (May 2015) |
253 ------------------------------ |
259 ------------------------------ |