| changeset 9238 | ad37b21c0dc6 |
| parent 9233 | 8c8399b9ecaa |
| child 9273 | 798673f65f02 |
--- a/doc-src/IsarRef/pure.tex Tue Jul 04 01:10:53 2000 +0200 +++ b/doc-src/IsarRef/pure.tex Tue Jul 04 01:11:42 2000 +0200 @@ -662,6 +662,10 @@ 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 facts. + \subsection{Goal statements}