• 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.
    03bb57a2
Name
Last commit
Last update
..
bench Loading commit data...
config Loading commit data...
coq-tactic Loading commit data...
core Loading commit data...
driver Loading commit data...
ide Loading commit data...
parser Loading commit data...
printer Loading commit data...
programs Loading commit data...
session Loading commit data...
tools Loading commit data...
transform Loading commit data...
util Loading commit data...
why3doc Loading commit data...
why3session Loading commit data...
whyml Loading commit data...
config.sh.in Loading commit data...
main.ml Loading commit data...
why3.ml Loading commit data...