--- 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}
--- a/src/Pure/pure_thy.ML Tue Jul 04 01:10:53 2000 +0200
+++ b/src/Pure/pure_thy.ML Tue Jul 04 01:11:42 2000 +0200
@@ -454,6 +454,7 @@
|> (#1 oo (add_defs o map Thm.no_attributes))
[("flexpair_def", "(t =?= u) == (t == u::'a::{})"),
("Goal_def", "GOAL (PROP A) == PROP A")]
+ |> (#1 o add_thmss [(("nothing", []), [])])
|> end_theory;
structure ProtoPure =