author | paulson |
Wed, 05 Mar 1997 09:59:55 +0100 | |
changeset 2721 | f08042e18c7d |
parent 2720 | 3490ef519a56 |
child 2722 | 3e07c20b967c |
src/HOL/Set.ML | file | annotate | diff | comparison | revisions |
--- 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";