added "numerals" theorems;
authorwenzelm
Thu Feb 01 20:43:41 2001 +0100 (2001-02-01)
changeset 1101871d624788ce2
parent 11017 241cbdf4134e
child 11019 e968e5bfe98d
added "numerals" theorems;
src/HOL/Integ/nat_bin.ML
     1.1 --- a/src/HOL/Integ/nat_bin.ML	Thu Feb 01 20:43:14 2001 +0100
     1.2 +++ b/src/HOL/Integ/nat_bin.ML	Thu Feb 01 20:43:41 2001 +0100
     1.3 @@ -290,8 +290,8 @@
     1.4  fun rename_numerals th = simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
     1.5  
     1.6  (*Maps #n to n for n = 0, 1, 2*)
     1.7 -val numeral_ss = 
     1.8 -    simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2];
     1.9 +bind_thms ("numerals", [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2]);
    1.10 +val numeral_ss = simpset() addsimps numerals;
    1.11  
    1.12  (** Nat **)
    1.13