diff options
| -rwxr-xr-x | doc/RefMan-pro.tex | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex index 3adecde1d5..b84d1b38a7 100755 --- a/doc/RefMan-pro.tex +++ b/doc/RefMan-pro.tex @@ -95,6 +95,10 @@ if the original goal has been opened using the {\tt Goal} command. Are equivalent to {\tt Save {\ident}.} \end{Variants} +\subsection{\tt Admitted.}\comindex{Admitted}\label{Admitted} +This command is available in interactive editing proof mode to give up +the current proof and declare the initial goal as an axiom. + \subsection{\tt Theorem {\ident} : {\form}.}\comindex{Theorem}\label{Theorem} This command switches to interactive editing proof mode and declares {\ident} as being the name of the original goal {\form}. When declared |