# HG changeset patch
# User paulson
# Date 963486288 -7200
# Node ID 342cbcb9c0d859f356b89804cfbadcd2a32958bd
# Parent  f1ad1ed0d110567441c81ae4b6e8f1ed6c72d8a1
added an important default rule

diff -r f1ad1ed0d110 -r 342cbcb9c0d8 src/ZF/subset.ML
--- a/src/ZF/subset.ML	Thu Jul 13 13:02:20 2000 +0200
+++ b/src/ZF/subset.ML	Thu Jul 13 13:04:48 2000 +0200
@@ -20,6 +20,7 @@
 Goal "cons(a,B)<=C <-> a:C & B<=C";
 by (Blast_tac 1);
 qed "cons_subset_iff";
+AddIffs [cons_subset_iff];
 
 (*A safe special case of subset elimination, adding no new variables 
   [| cons(a,B) <= C; [| a : C; B <= C |] ==> R |] ==> R *)