Added global let-simplification rule.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Numeral.ML	Sun Feb 20 09:32:06 2000 +0100
@@ -0,0 +1,10 @@
+(*  Title:      HOL/Numeral.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+*)
+
+(*Unfold all "let"s involving constants*)
+Goalw [Let_def] "Let (number_of v) f == f (number_of v)";
+by(Simp_tac 1);
+qed "Let_number_of";
+Addsimps [Let_number_of];