• Andrei Paskevich's avatar
    revise split transformations · 03bb57a2
    Andrei Paskevich authored
    Provide nine transformations: split_(goal|all|premise)_(full|right|wp).
    split_*_full splits as far as it can, split_*_right produces linear
    number of subformulas, split_*_wp stops at the "stop_split" label.
    The name "split_goal" is kept for compatibility with older session
    files and denotes the same transformation as "split_goal_wp".
    Thanks to Johannes Kanig for the suggestion.
introduction.ml 3.27 KB