# HG changeset patch
# User lcp
# Date 796564895 -7200
# Node ID 2e50c5124ca31fd0905474634efc61cfdcd4d24b
# Parent  4fb1d099ba457751c84e33f1dd644fd9ce86559b
Added comment about why mem_irrefl should not be a safeE.

diff -r 4fb1d099ba45 -r 2e50c5124ca3 src/ZF/upair.ML
--- a/src/ZF/upair.ML	Thu Mar 30 13:54:41 1995 +0200
+++ b/src/ZF/upair.ML	Thu Mar 30 14:01:35 1995 +0200
@@ -314,7 +314,9 @@
 qed_goal "succ_inject_iff" ZF.thy "succ(m) = succ(n) <-> m=n"
  (fn _=> [ (fast_tac (FOL_cs addSEs [succ_inject]) 1) ]);
 
-(*UpairI1/2 should become UpairCI;  mem_irrefl as a hazE? *)
+(*UpairI1/2 should become UpairCI? 
+  mem_irrefl should NOT be added as an elim-rule here; 
+      it would be tried on most goals, making proof slower!*)
 val upair_cs = lemmas_cs
   addSIs [singletonI, DiffI, IntI, UnCI, consCI, succCI, UpairI1,UpairI2]
   addSEs [singletonE, DiffE, IntE, UnE, consE, succE, UpairE];