src/HOL/Nat.ML
changeset 10450 60ddd5fdf93b
parent 10173 1d097572d23b
child 10558 09a91221ced1
     1.1 --- a/src/HOL/Nat.ML	Fri Nov 10 19:17:46 2000 +0100
     1.2 +++ b/src/HOL/Nat.ML	Fri Nov 10 19:18:14 2000 +0100
     1.3 @@ -610,6 +610,9 @@
     1.4  qed "diff_mult_distrib2" ;
     1.5  (*NOT added as rewrites, since sometimes they are used from right-to-left*)
     1.6  
     1.7 +bind_thms ("nat_distrib",
     1.8 +  [add_mult_distrib, add_mult_distrib2, diff_mult_distrib, diff_mult_distrib2]);
     1.9 +
    1.10  
    1.11  (*** Monotonicity of Multiplication ***)
    1.12