Hi, I have a theorem of the form:
!x1 x2 ... x(i-1) xi x(i+1) ... xn. t and I'd like to instantiate xi to another term, say y, without touching other universally quantified variables, namely, I want to rewrite it to: !x1 x2 ... x(i-1) x(i+1) ... xn. t[y/xi] Is there a handy operation for this, any version of SPECL, or I can change the order of xs? 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
