src/ZF/upair.ML
changeset 985 2e50c5124ca3
parent 834 ad1d0eb0ee82
child 1017 6a402dc505cf
--- 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];