# HG changeset patch
# User nipkow
# Date 951035526 -3600
# Node ID fffae6147cf7ac620fa6a47916cde226a16f7828
# Parent  699d4ad2ced3e8324a3e31aba1e9329913d6b263
Added global let-simplification rule.

diff -r 699d4ad2ced3 -r fffae6147cf7 src/HOL/Numeral.ML
--- /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];