New version of InterE, like its ZF counterpart
authorpaulson
Wed, 05 Mar 1997 09:59:55 +0100
changeset 2721 f08042e18c7d
parent 2720 3490ef519a56
child 2722 3e07c20b967c
New version of InterE, like its ZF counterpart
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";