equal
deleted
inserted
replaced
282 * Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous |
282 * Subgoal.SUBPROOF and Subgoal.FOCUS combinators use anonymous |
283 quasi-bound variables (like the Simplifier), instead of accidentally |
283 quasi-bound variables (like the Simplifier), instead of accidentally |
284 named local fixes. This has the potential to improve stability of proof |
284 named local fixes. This has the potential to improve stability of proof |
285 tools, but can also cause INCOMPATIBILITY for tools that don't observe |
285 tools, but can also cause INCOMPATIBILITY for tools that don't observe |
286 the proof context discipline. |
286 the proof context discipline. |
|
287 |
|
288 |
|
289 *** System *** |
|
290 |
|
291 * Poly/ML 5.5.3 runs natively on x86-windows, with somewhat larger heap |
|
292 space than former x86-cygwin. |
287 |
293 |
288 |
294 |
289 |
295 |
290 New in Isabelle2015 (May 2015) |
296 New in Isabelle2015 (May 2015) |
291 ------------------------------ |
297 ------------------------------ |