added "nothing" (empty list of theorems);

--- 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 =