nat_distrib;
authorwenzelm
Fri Nov 10 19:18:14 2000 +0100 (2000-11-10)
changeset 1045060ddd5fdf93b
parent 10449 088aa7bd3154
child 10451 226d474e644d
nat_distrib;
src/HOL/Nat.ML
     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