Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
nat_distrib;
authorwenzelm
Fri, 10 Nov 2000 19:18:14 +0100
changeset 10450 60ddd5fdf93b
parent 10449 088aa7bd3154
child 10451 226d474e644d
nat_distrib;
src/HOL/Nat.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nat.ML	Fri Nov 10 19:17:46 2000 +0100
+++ b/src/HOL/Nat.ML	Fri Nov 10 19:18:14 2000 +0100
@@ -610,6 +610,9 @@
 qed "diff_mult_distrib2" ;
 (*NOT added as rewrites, since sometimes they are used from right-to-left*)
 
+bind_thms ("nat_distrib",
+  [add_mult_distrib, add_mult_distrib2, diff_mult_distrib, diff_mult_distrib2]);
+
 
 (*** Monotonicity of Multiplication ***)
isabelle