# HG changeset patch
# User lcp
# Date 783877181 -3600
# Node ID a1586fa1b755a8486c3e801f744b73aec858cfb8
# Parent  c7d592f6312a59ef488b3b9349bf9b9a82259908
ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)

diff -r c7d592f6312a -r a1586fa1b755 src/ZF/ex/misc.ML
--- a/src/ZF/ex/misc.ML	Thu Nov 03 16:05:22 1994 +0100
+++ b/src/ZF/ex/misc.ML	Thu Nov 03 16:39:41 1994 +0100
@@ -91,10 +91,10 @@
 
 (** A characterization of functions, suggested by Tobias Nipkow **)
 
-goalw ZF.thy [Pi_def]
+goalw ZF.thy [Pi_def, function_def]
     "r: domain(r)->B  <->  r <= domain(r)*B & (ALL X. r `` (r -`` X) <= X)";
 by (safe_tac ZF_cs);
-by (fast_tac (ZF_cs addSDs [bspec RS ex1_equalsE]) 1);
+by (fast_tac ZF_cs 1);
 by (eres_inst_tac [("x", "{y}")] allE 1);
 by (fast_tac ZF_cs 1);
 result();
@@ -175,29 +175,14 @@
 
 (** Yet another example... **)
 
-goalw (merge_theories(Sum.thy,Perm.thy)) [bij_def,inj_def,surj_def]
+goal (merge_theories(Sum.thy,Perm.thy))
     "(lam Z:Pow(A+B). <{x:A. Inl(x):Z}, {y:B. Inr(y):Z}>) \
 \    : bij(Pow(A+B), Pow(A)*Pow(B))";
-by (DO_GOAL
-      [rtac IntI,
-       DO_GOAL
-	 [rtac CollectI,
-	  fast_tac (ZF_cs addSIs [lam_type]),
-	  simp_tac ZF_ss,
-	  fast_tac (eq_cs addSEs [sumE]
-			  addEs  [equalityD1 RS subsetD RS CollectD2,
-				  equalityD2 RS subsetD RS CollectD2])],
-       DO_GOAL
-	 [rtac CollectI,
-	  fast_tac (ZF_cs addSIs [lam_type]),
-	  simp_tac ZF_ss,
-	  K(safe_tac ZF_cs),
-	  res_inst_tac [("x", "{Inl(u). u: ?U} Un {Inr(v). v: ?V}")] bexI,
-	  DO_GOAL
-	    [res_inst_tac [("t", "Pair")] subst_context2,
-	    fast_tac (sum_cs addSIs [equalityI]),
-	    fast_tac (sum_cs addSIs [equalityI])],
-	  DO_GOAL [fast_tac sum_cs]]] 1);
+by (res_inst_tac [("d", "split(%X Y.{Inl(x).x:X} Un {Inr(y).y:Y})")] 
+    lam_bijective 1);
+by (TRYALL (etac SigmaE));
+by (ALLGOALS (asm_simp_tac ZF_ss));
+by (ALLGOALS (fast_tac (sum_cs addSIs [equalityI])));
 val Pow_bij = result();
 
 writeln"Reached end of file.";