Hi, Is there a theorem that I can move (existential) quantifiers to the very front of an assumption? For example,
goal ---- p ==> ?x y. (?u v. q u v \/ m u v) /\ t x y I'd like to get something like: goal ---- p ==> (q u v \/ m u v) /\ t x y Thanks a lot. Lu ------------------------------------------------------------------------------ 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
