Skip to content

I
Iris
Commit c98ea2a5 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Document iFrame without arguments.

parent efc93d9c
Pipeline #2549 passed with stage
    in 3 minutes and 56 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 3 additions and 1 deletion
    ProofMode.md
    View file @ c98ea2a5
    ......@@ -70,7 +70,9 @@ Elimination of logical connectives
    Separating logic specific tactics
    ---------------------------------
    - `iFrame "H0 ... Hn"` : cancel the hypotheses `H0 ... Hn` in the goal.
    - `iFrame "H0 ... Hn"` : cancel the hypotheses `H0 ... Hn` in the goal. When
    `iFrame` is called without arguments, it attempts to frame all spatial
    hypotheses.
    - `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into
    `H : P1 ★ P2`.
    ......
    Markdown is supported
    0% or
    You are about to add 0 people to the discussion. Proceed with caution.
    Finish editing this message first!
    Please register or to comment