# HG changeset patch
# User wenzelm
# Date 962665902 -7200
# Node ID ad37b21c0dc6f58944d0ec04917a70b5c2825507
# Parent  161fb7f00414b74d53d2b0b2e59e14f314d2329a
added "nothing" (empty list of theorems);

diff -r 161fb7f00414 -r ad37b21c0dc6 doc-src/IsarRef/pure.tex
--- 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}
 
diff -r 161fb7f00414 -r ad37b21c0dc6 src/Pure/pure_thy.ML
--- 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 =