new sproofs

[Jazzpirate]

should be merged in conjunction with grep magic in mikomh ;)

[kohlhase]

In MathHub/MiKoMH/GenCS/source/pl0/mod/subst-value-lemma.en.tex I have

        \begin{spfstep}
          This is the case, iff $\Evaluation\psi\bC=\semfalse$ or
          $\Evaluation\psi\bD=\semtrue$ \spfjust[method=byIH]{by {\premise{IH}} ($\bC$ and
            $\bD$ have smaller depth than $\bA$).}
        \end{spfstep}

How do we do the \sfpjust is that just kept? The documentation still mentions it.

[kohlhase]

I am preparing the replacement script while we are discussing this.

[Jazzpirate]

How do we do the \sfpjust is that just kept? The documentation still mentions it.

That still exists, although it is basically a nullop currently. For \spfjust to do something meaningfull, we would need an ontology of (basically) "proof tactics". \premise however should certainly go, and probably semantically attached to the \spfjust (or I'm confused about its semantics)

[kohlhase]

\yield and \justarg still need to be documented as a function block.

[kohlhase]

That still exists, although it is basically a nullop currently. For \spfjust to do something meaningfull, we would need an ontology of (basically) "proof tactics". \premise however should certainly go, and probably semantically attached to the \spfjust (or I'm confused about its semantics)

I think we should think about (and prossibly redesign) this, if we touch the sproof package. Otherwise we will have to have another go at it.

In particular, we should think about functionality we want to attach to all the semantic annotations to justify them. Otherwise I can just eliminate them.