NEWS
changeset 63656 fac9097dc772
parent 63649 50cadecbe5bc
child 63669 256fc20716f2
equal deleted inserted replaced
63655:d31650b377c4 63656:fac9097dc772
    49 context. Unlike "context includes ... begin", the effect of 'unbundle'
    49 context. Unlike "context includes ... begin", the effect of 'unbundle'
    50 on the target context persists, until different declarations are given.
    50 on the target context persists, until different declarations are given.
    51 
    51 
    52 * Splitter in simp, auto and friends:
    52 * Splitter in simp, auto and friends:
    53 - The syntax "split add" has been discontinued, use plain "split".
    53 - The syntax "split add" has been discontinued, use plain "split".
    54 - For situations with many nested conditional or case expressions,
    54 - For situations with many conditional or case expressions,
    55 there is an alternative splitting strategy that can be much faster.
    55 there is an alternative splitting strategy that can be much faster.
    56 It is selected by writing "split!" instead of "split". It applies
    56 It is selected by writing "split!" instead of "split". It applies
    57 safe introduction and elimination rules after each split rule.
    57 safe introduction and elimination rules after each split rule.
    58 As a result the subgoal may be split into several subgoals.
    58 As a result the subgoal may be split into several subgoals.
    59 
    59