# HG changeset patch
# User lcp
# Date 789846126 -3600
# Node ID e50a32a4f66932d00d19ddbe19aeaa1f6a9ad90d
# Parent  c4566750dc12dde23f258667fcfb4be2772fb9c1
Proved cadd_cmult_distrib.

diff -r c4566750dc12 -r e50a32a4f669 src/ZF/Cardinal_AC.ML
--- 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);