Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Dan Frumin
iris-coq
Commits
7d30ec04
Commit
7d30ec04
authored
Jul 05, 2016
by
Robbert Krebbers
Browse files
Fix typo.
parent
1c814611
Changes
1
Hide whitespace changes
Inline
Side-by-side
ProofMode.md
View file @
7d30ec04
...
...
@@ -122,7 +122,7 @@ appear at the top level:
-
`>`
: introduce a later (which strips laters from all hypotheses).
-
`{H1 ... Hn}`
: clear
`H1 ... Hn`
.
-
`{$H1 ... $Hn}`
: frame
`H1 ... Hn`
(this pattern can be mixed with the
previous pattern, e.g.,
`{$H1 H2
#
H3}`
).
previous pattern, e.g.,
`{$H1 H2
$
H3}`
).
-
`/=`
: perform
`simpl`
.
-
`*`
: introduce all universal quantifiers.
-
`**`
: introduce all universal quantifiers, as well as all arrows and wands.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment