Hi Jianjun, > I have difficulty proving something like
> `!x y z. ((x UNION y = z) /\ DISJOINT x y) ==> (x = z DIFF y)`. > Any help please? Simple equalities on sets usually fall over if you attack them with extensionality and METIS_TAC. In this case, the tactic SRW_TAC [][DISJOINT_DEF, EXTENSION] THEN METIS_TAC [] does the job (assuming that you have pred_setTheory open to pick up the theorems DISJOINT_DEF and EXTENSION). Michael. ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
