Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

1 files changed, 44 insertions, 10 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 7af87a399a..c37367de5b 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -157,21 +157,36 @@ in Section~\ref{ProofWith}.
   
   Use only section variables occurring in the statement.
 
-\variant {\tt Proof using -(} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).}
+\variant {\tt Proof using Type*.} 
+  
+  The {\tt *} operator computes the forward transitive closure.
+  E.g. if the variable {\tt H} has type {\tt p < 5} then {\tt H} is
+  in {\tt p*} since {\tt p} occurs in the type of {\tt H}.
+  {\tt Type* } is the forward transitive closure of the entire set of
+  section variables occurring in the statement.
+
+\variant {\tt Proof using -( \ident$_1$} {\ldots} {\tt \ident$_n$  ).}
   
   Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}.
 
-\variant {\tt Proof using }  {\emph collection$_1$} {\tt + } {\emph collection$_2$} {\tt .}
-\variant {\tt Proof using }  {\emph collection$_1$} {\tt - } {\emph collection$_2$} {\tt .}
-\variant {\tt Proof using }  {\emph collection$_1$} {\tt - (} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).}
+\variant {\tt Proof using \nterm{collection}$_1$ + \nterm{collection}$_2$ .}
+
+\variant {\tt Proof using \nterm{collection}$_1$ - \nterm{collection}$_2$ .}
+
+\variant {\tt Proof using \nterm{collection} - ( \ident$_1$} {\ldots} {\tt \ident$_n$ ).}
 
-  Use section variables being in the set union or set difference of the two
-  colelctions.  See Section~\ref{Collection} to know how to form a named
+\variant {\tt Proof using \nterm{collection} * .}
+
+  Use section variables being, respectively, in the set union, set difference,
+  set complement, set forward transitive closure.
+  See Section~\ref{Collection} to know how to form a named
   collection.
+  The {\tt *} operator binds stronger than {\tt +} and {\tt -}.
 
 \subsubsection{{\tt Proof using} options}
-\comindex{Default Proof Using}
-\comindex{Suggest Proof Using}
+\optindex{Default Proof Using}
+\optindex{Suggest Proof Using}
+% \optindex{Proof Using Clear Unused}
 
 The following options modify the behavior of {\tt Proof using}.
 
@@ -186,11 +201,17 @@ The following options modify the behavior of {\tt Proof using}.
   When {\tt Qed} is performed, suggest a {\tt using} annotation if
   the user did not provide one.
 
+% \variant{\tt Unset Proof Using Clear Unused.}
+% 
+%   When {\tt Proof using a} all section variables but for {\tt a} and
+%   the variables used in the type of {\tt a} are cleared.
+%   This option can be used to turn off this behavior.
+% 
 \subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}}
 \comindex{Collection}\label{Collection}
 
 The command {\tt Collection} can be used to name a set of section hypotheses,
-with the purpose of making {\tt Proof using} annotations more compat.
+with the purpose of making {\tt Proof using} annotations more compact.
 
 \variant {\tt Collection Some := x y z.}
 
@@ -209,7 +230,7 @@ with the purpose of making {\tt Proof using} annotations more compat.
 \variant {\tt Collection Many := Fewer - (x y).}
 
   Define the collection named "Many" containing the set difference
-  of "Fewer" and the unamed collection {\tt x y}.
+  of "Fewer" and the unnamed collection {\tt x y}.
 
 \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
 
@@ -386,6 +407,19 @@ Proof.
 
 \end{ErrMsgs}
 
+The bullet behavior can be controlled by the following commands.
+
+\begin{quote}
+Set Bullet Behavior "None".
+\end{quote}
+
+This makes bullets inactive.
+
+\begin{quote}
+Set Bullet Behavior "Strict Subproofs".
+\end{quote}
+
+This makes bullets active (this is the default behavior).
 
 \section{Requesting information}