New version of InterE, like its ZF counterpart
authorpaulson
Wed Mar 05 09:59:55 1997 +0100 (1997-03-05)
changeset 2721f08042e18c7d
parent 2720 3490ef519a56
child 2722 3e07c20b967c
New version of InterE, like its ZF counterpart
src/HOL/Set.ML
     1.1 --- a/src/HOL/Set.ML	Wed Mar 05 09:59:24 1997 +0100
     1.2 +++ b/src/HOL/Set.ML	Wed Mar 05 09:59:55 1997 +0100
     1.3 @@ -569,7 +569,7 @@
     1.4  
     1.5  (*"Classical" elimination rule -- does not require proving X:C *)
     1.6  val major::prems = goalw Set.thy [Inter_def]
     1.7 -    "[| A : Inter(C);  A:X ==> R;  X~:C ==> R |] ==> R";
     1.8 +    "[| A : Inter(C);  X~:C ==> R;  A:X ==> R |] ==> R";
     1.9  by (rtac (major RS INT_E) 1);
    1.10  by (REPEAT (eresolve_tac prems 1));
    1.11  qed "InterE";