• MARCHE Claude's avatar
    Improved copy-paste functionality · a97edee6
    MARCHE Claude authored
    - copy from a transformation to a proof node works, adding
      the transformation below the target node
    - when copied transformation as less or more subgoals, then
      only the first subgoals are copied
    - explicit error message in case of invalid copy
demo-itp.mlw 2.95 KB