# HG changeset patch
# User lcp
# Date 788196722 -3600
# Node ID 60d850cc5fe62d16c41027fd0be9c9a4df27f32e
# Parent  18240b5d8a062948731504eda1807b98b5f2118d
Added Krzysztof's theorem pred_Memrel

diff -r 18240b5d8a06 -r 60d850cc5fe6 src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Fri Dec 23 16:31:23 1994 +0100
+++ b/src/ZF/OrderType.ML	Fri Dec 23 16:32:02 1994 +0100
@@ -27,6 +27,11 @@
 by (fast_tac (eq_cs addEs [Ord_trans]) 1);
 qed "lt_eq_pred";
 
+goalw OrderType.thy [pred_def,Memrel_def] 
+      "!!A x. x:A ==> pred(A, x, Memrel(A)) = {b:A. b:x}";
+by (fast_tac eq_cs 1);
+qed "pred_Memrel";
+
 goal OrderType.thy
     "!!i. [| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R";
 by (forward_tac [lt_eq_pred] 1);
@@ -171,8 +176,8 @@
 by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1);
 by (resolve_tac [Ord_iso_implies_eq] 1
     THEN REPEAT (eresolve_tac [Ord_ordertype] 1));
-by (deepen_tac (ZF_cs addIs [ord_iso_trans, ord_iso_sym]
-                    addSEs [ordertype_ord_iso]) 0 1);
+by (deepen_tac (ZF_cs addIs  [ord_iso_trans, ord_iso_sym]
+                      addSEs [ordertype_ord_iso]) 0 1);
 qed "ordertype_eq";