# HG changeset patch
# User wenzelm
# Date 981056621 -3600
# Node ID 71d624788ce2723966801825d1120984d201e6e0
# Parent  241cbdf4134e332c98e4d30a6857ef557aec23b8
added "numerals" theorems;

diff -r 241cbdf4134e -r 71d624788ce2 src/HOL/Integ/nat_bin.ML
--- a/src/HOL/Integ/nat_bin.ML	Thu Feb 01 20:43:14 2001 +0100
+++ b/src/HOL/Integ/nat_bin.ML	Thu Feb 01 20:43:41 2001 +0100
@@ -290,8 +290,8 @@
 fun rename_numerals th = simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
 
 (*Maps #n to n for n = 0, 1, 2*)
-val numeral_ss = 
-    simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2];
+bind_thms ("numerals", [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2]);
+val numeral_ss = simpset() addsimps numerals;
 
 (** Nat **)