Proved cadd_cmult_distrib.

--- a/src/ZF/Cardinal_AC.ML	Wed Jan 11 18:30:37 1995 +0100
+++ b/src/ZF/Cardinal_AC.ML	Wed Jan 11 18:42:06 1995 +0100
@@ -48,6 +48,14 @@
 by (REPEAT_SOME assume_tac);
 qed "cmult_assoc";
 
+goal Cardinal_AC.thy "(i |+| j) |*| k = (i |*| k) |+| (j |*| k)";
+by (resolve_tac [AC_well_ord RS exE] 1);
+by (resolve_tac [AC_well_ord RS exE] 1);
+by (resolve_tac [AC_well_ord RS exE] 1);
+by (resolve_tac [well_ord_cadd_cmult_distrib] 1);
+by (REPEAT_SOME assume_tac);
+qed "cadd_cmult_distrib";
+
 goal Cardinal_AC.thy "!!A. InfCard(|A|) ==> A*A eqpoll A";
 by (resolve_tac [AC_well_ord RS exE] 1);
 by (eresolve_tac [well_ord_InfCard_square_eq] 1);