From b49d803286ba9ed711313702bb4269c5e9c516fa Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Thu, 18 Dec 2014 16:35:46 +0100
Subject: Proof using: New vernacular to name sets of section variables

---
 doc/refman/RefMan-pro.tex | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 8d69f1682..789297fb4 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -177,6 +177,25 @@ 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}
+
+The command {\tt Package} 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.}
+
+  Define the package named "Some" containing {\tt x y} and {\tt z} 
+
+\variant {\tt Package Fewer := Some - x.} 
+  
+  Define the package named "Fewer" containing only {\tt x y} 
+
+\variant {\tt Package Many := Fewer + Some.} 
+  
+  Define the package named "Many" containing the union of the elements
+  of "Fewer" and "Some", namely {\tt x y z}. 
+
 \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
 
 This command cancels the current proof development, switching back to
-- 
cgit v1.2.3