# HG changeset patch
# User lcp
# Date 799502599 -7200
# Node ID fdaf39a47a2b7d459346c16cbe77c707778fd55d
# Parent  f55f54a032ce0e86cea29fe8a9550455fa4fa746
Changed some definitions and proofs to use pattern-matching.

diff -r f55f54a032ce -r fdaf39a47a2b src/ZF/Cardinal_AC.ML
--- a/src/ZF/Cardinal_AC.ML	Wed May 03 13:55:05 1995 +0200
+++ b/src/ZF/Cardinal_AC.ML	Wed May 03 14:03:19 1995 +0200
@@ -114,7 +114,7 @@
 by (fast_tac (ZF_cs addSIs [Least_le RS lt_trans1 RS ltD, ltI]
                     addSEs [LeastI, Ord_in_Ord]) 2);
 by (res_inst_tac [("c", "%z. <LEAST i. z:X(i), f ` (LEAST i. z:X(i)) ` z>"),
-		  ("d", "split(%i j. converse(f`i) ` j)")] 
+		  ("d", "%<i,j>. converse(f`i) ` j")] 
 	lam_injective 1);
 (*Instantiate the lemma proved above*)
 by (ALLGOALS ball_tac);