--- a/doc-src/IsarRef/pure.tex Fri Oct 28 22:27:41 2005 +0200
+++ b/doc-src/IsarRef/pure.tex Fri Oct 28 22:27:44 2005 +0200
@@ -1026,13 +1026,14 @@
object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and
\ref{ch:logics}).
-\indexisarmeth{$-$}\indexisarmeth{assumption}
+\indexisarmeth{$-$}\indexisarmeth{fact}\indexisarmeth{assumption}
\indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{iprover}
\indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
\indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
\indexisaratt{OF}\indexisaratt{of}\indexisaratt{where}
\begin{matharray}{rcl}
- & : & \isarmeth \\
+ fact & : & \isarmeth \\
assumption & : & \isarmeth \\
this & : & \isarmeth \\
rule & : & \isarmeth \\
@@ -1047,6 +1048,8 @@
\end{matharray}
\begin{rail}
+ 'fact' thmrefs?
+ ;
'rule' thmrefs?
;
'iprover' ('!' ?) (rulemod *)
@@ -1073,6 +1076,14 @@
\emph{do-nothing} proof step would be ``$\PROOF{-}$'' rather than
$\PROOFNAME$ alone.
+\item [$fact~\vec a$] composes any previous fact from $\vec a$ (or implicitly
+ from the current proof context) modulo matching of schematic type and term
+ variables. The rule structure is not taken into account, i.e.\ meta-level
+ implication is considered atomic. This is the same principle underlying
+ literal facts (cf.\ \S\ref{sec:syn-att}): ``$\HAVE{}{\phi}~\BY{fact}$'' is
+ equivalent to ``$\NOTE{}{\backquote\phi\backquote}$'' provided that $\edrv
+ \phi$ is an instance of some known $\edrv \phi$ in the proof context.
+
\item [$assumption$] solves some goal by a single assumption step. All given
facts are guaranteed to participate in the refinement; this means there may
be only $0$ or $1$ in the first place. Recall that $\QEDNAME$ (see