# HG changeset patch
# User wenzelm
# Date 1014835435 -3600
# Node ID 6373b4d0932593f2fe001aa2cb2a823effa208ce
# Parent  c8a97eb1e3c7acd4433adba050a18aeaa1a17097
'using' command;

diff -r c8a97eb1e3c7 -r 6373b4d09325 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Wed Feb 27 19:43:20 2002 +0100
+++ b/doc-src/IsarRef/pure.tex	Wed Feb 27 19:43:55 2002 +0100
@@ -660,22 +660,28 @@
 \subsection{Facts and forward chaining}
 
 \indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
+\indexisarcmd{using}
 \begin{matharray}{rcl}
   \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
   \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
   \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
   \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
+  \isarcmd{using} & : & \isartrans{proof(prove)}{proof(prove)} \\
 \end{matharray}
 
 New facts are established either by assumption or proof of local statements.
 Any fact will usually be involved in further proofs, either as explicit
 arguments of proof methods, or when forward chaining towards the next goal via
-$\THEN$ (and variants).  Note that the special theorem name
-$this$\indexisarthm{this} refers to the most recently established facts.
+$\THEN$ (and variants); $\FROMNAME$ and $\WITHNAME$ are composite forms
+involving $\NOTE$.  The $\USINGNAME$ elements allows to augment the collection
+of used facts \emph{after} a goal has been stated.  Note that the special
+theorem name $this$\indexisarthm{this} refers to the most recently established
+facts, but only \emph{before} issuing a follow-up claim.
+
 \begin{rail}
   'note' (thmdef? thmrefs + 'and')
   ;
-  ('from' | 'with') (thmrefs + 'and')
+  ('from' | 'with' | 'using') (thmrefs + 'and')
   ;
 \end{rail}
 
@@ -695,20 +701,25 @@
   equivalent to $\FROM{this}$.
 \item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~this}$; thus the forward
   chaining is from earlier facts together with the current ones.
+\item [$\USING{\vec b}$] augments the facts being currently indicated for use
+  in a subsequent refinement step (such as $\APPLYNAME$ or $\PROOFNAME$).
 \end{descr}
 
-Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth-att}) expect
-multiple facts to be given in their proper order, corresponding to a prefix of
-the premises of the rule involved.  Note that positions may be easily skipped
-using something like $\FROM{\Text{\texttt{_}}~a~b}$, for example.  This
-involves the trivial rule $\PROP\psi \Imp \PROP\psi$, which happens to be
-bound in Isabelle/Pure as ``\texttt{_}''
-(underscore).\indexisarthm{_@\texttt{_}}
-
 Forward chaining with an empty list of theorems is the same as not chaining.
 Thus $\FROM{nothing}$ has no effect apart from entering $prove(chain)$ mode,
 since $nothing$\indexisarthm{nothing} is bound to the empty list of theorems.
 
+Basic proof methods (such as $rule$) expect multiple facts to be given in
+their proper order, corresponding to a prefix of the premises of the rule
+involved.  Note that positions may be easily skipped using something like
+$\FROM{\Text{\texttt{_}}~a~b}$, for example.  This involves the trivial rule
+$\PROP\psi \Imp \PROP\psi$, which happens to be bound in Isabelle/Pure as
+``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}}
+
+Automated methods (such as $simp$ or $auto$) just insert any given facts
+before their usual operation.  Depending on the kind of procedure involved,
+the order of facts is less significant here.
+
 
 \subsection{Goal statements}
 
@@ -735,24 +746,25 @@
 conjunction (printed as \verb,&&,), which is automatically split into the
 corresponding number of sub-goals prior to any initial method application, via
 $\PROOFNAME$ (\S\ref{sec:proof-steps}) or $\APPLYNAME$
-(\S\ref{sec:tactic-commands}).\footnote{Deviating from the latter principle,
-  the $induct$ method covered in \S\ref{sec:cases-induct-meth} acts on
-  multiple claims simultaneously.}
+(\S\ref{sec:tactic-commands}).\footnote{The $induct$ method covered in
+  \S\ref{sec:cases-induct-meth} acts on multiple claims simultaneously.}
+
+Claims at the theory level may be either in ``short'' or ``long'' form.  A
+short goal merely consists of several simultaneous propositions (often just
+one).  A long goal includes an explicit context specification for the
+subsequent conclusions, involving local parameters; here the role of each part
+of the statement is explicitly marked by separate keywords (see also
+\S\ref{sec:locale}).
 
 \begin{rail}
-  ('lemma' | 'theorem' | 'corollary') goalprefix goal
+  ('lemma' | 'theorem' | 'corollary') locale? (shortgoal | longgoal)
   ;
-  ('have' | 'show' | 'hence' | 'thus') goal
-  ;
-
-  goal: (props + 'and')
+  ('have' | 'show' | 'hence' | 'thus') shortgoal
   ;
-
-  goalprefix: thmdecl? locale? context?
+  
+  shortgoal: (props + 'and')
   ;
-  locale: '(' 'in' name ')'
-  ;
-  context: '(' (contextelem +) ')'
+  longgoal: thmdecl? (contextelem *) 'shows' shortgoal
   ;
 \end{rail}
 
diff -r c8a97eb1e3c7 -r 6373b4d09325 doc-src/isar.sty
--- a/doc-src/isar.sty	Wed Feb 27 19:43:20 2002 +0100
+++ b/doc-src/isar.sty	Wed Feb 27 19:43:55 2002 +0100
@@ -39,6 +39,7 @@
 \newcommand{\NOTENAME}{\isarkeyword{note}}
 \newcommand{\FROMNAME}{\isarkeyword{from}}
 \newcommand{\WITHNAME}{\isarkeyword{with}}
+\newcommand{\USINGNAME}{\isarkeyword{using}}
 \newcommand{\FIXNAME}{\isarkeyword{fix}}
 \newcommand{\ASSUMENAME}{\isarkeyword{assume}}
 \newcommand{\PRESUMENAME}{\isarkeyword{presume}}
@@ -74,6 +75,7 @@
 \newcommand{\NOTE}[2]{\NOTENAME~\ifthenelse{\equal{}{#1}}{}{#1=}#2}
 \newcommand{\FROM}[1]{\FROMNAME~#1}
 \newcommand{\WITH}[1]{\WITHNAME~#1}
+\newcommand{\USING}[1]{\USINGNAME~#1}
 \newcommand{\FIX}[1]{\FIXNAME~#1}
 \newcommand{\ASSUME}[2]{\ASSUMENAME\I@optname{#1}~#2}
 \newcommand{\PRESUME}[2]{\PRESUMENAME\I@optname{#1}~#2}