--- a/src/HOL/Set.ML Tue Jan 30 15:19:20 1996 +0100
+++ b/src/HOL/Set.ML Tue Jan 30 15:24:36 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOL/set
+(* Title: HOL/set
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
For set.thy. Set theory for higher-order logic. A set is simply a predicate.
@@ -339,7 +339,7 @@
\ (UN x:A. C(x)) = (UN x:B. D(x))";
by (REPEAT (etac UN_E 1
ORELSE ares_tac ([UN_I,equalityI,subsetI] @
- (prems RL [equalityD1,equalityD2] RL [subsetD])) 1));
+ (prems RL [equalityD1,equalityD2] RL [subsetD])) 1));
qed "UN_cong";