Better doc and a few fixes for Proof using.

1 files changed, 25 insertions, 10 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 789297fb4..4084424e8 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -153,6 +153,7 @@ in Section~\ref{ProofWith}.
   Use all section variables.
 
 \variant {\tt Proof using Type.} 
+\variant {\tt Proof using.} 
   
   Use only section variables occurring in the statement.
 
@@ -160,6 +161,14 @@ in Section~\ref{ProofWith}.
   
   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 ).}
+
+  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
+  collection.
+
 \subsubsection{{\tt Proof using} options}
 \comindex{Default Proof Using}
 \comindex{Suggest Proof Using}
@@ -177,24 +186,30 @@ 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.
 
-\subsubsection[\tt Package]{Name a set of section hypotheses for {\tt Proof using}}
-\comindex{Package}
+\subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}}
+\comindex{Collection}\label{Collection}
 
-The command {\tt Package} can be used to name a set of section hypotheses,
+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.
 
-\variant {\tt Package Some := x y z.}
+\variant {\tt Collection Some := x y z.}
 
-  Define the package named "Some" containing {\tt x y} and {\tt z} 
+  Define the collection named "Some" containing {\tt x y} and {\tt z} 
 
-\variant {\tt Package Fewer := Some - x.} 
+\variant {\tt Collection Fewer := Some - x.} 
   
-  Define the package named "Fewer" containing only {\tt x y} 
+  Define the collection named "Fewer" containing only {\tt x y} 
 
-\variant {\tt Package Many := Fewer + Some.} 
+\variant {\tt Collection Many := Fewer + Some.} 
+\variant {\tt Collection Many := Fewer - Some.} 
   
-  Define the package named "Many" containing the union of the elements
-  of "Fewer" and "Some", namely {\tt x y z}. 
+  Define the collection named "Many" containing the set union or set difference
+  of "Fewer" and "Some".
+
+\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}.
 
 \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}