# HG changeset patch
# User paulson
# Date 857552395 -3600
# Node ID f08042e18c7d1dd867133ff898f4393d53b91b78
# Parent  3490ef519a56238a2d4a4fe048f60a43b128d212
New version of InterE, like its ZF counterpart

diff -r 3490ef519a56 -r f08042e18c7d src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed Mar 05 09:59:24 1997 +0100
+++ b/src/HOL/Set.ML	Wed Mar 05 09:59:55 1997 +0100
@@ -569,7 +569,7 @@
 
 (*"Classical" elimination rule -- does not require proving X:C *)
 val major::prems = goalw Set.thy [Inter_def]
-    "[| A : Inter(C);  A:X ==> R;  X~:C ==> R |] ==> R";
+    "[| A : Inter(C);  X~:C ==> R;  A:X ==> R |] ==> R";
 by (rtac (major RS INT_E) 1);
 by (REPEAT (eresolve_tac prems 1));
 qed "InterE";