The file share/to_poly_solve/to_poly_solve_extra.lisp has (my) versions of simplifying 'if,' 'and,' and 'or.' --Barton ________________________________ Robert, I have been working to develop a theorem prover in Maxima based on old Lisp codes. I'd be happy to help in boolsimp - it would help me to understand the "maxima way".