src/HOL/SMT/Examples/cert/z3_linarith_05
2009-10-20 boehmes added proof reconstructon for Z3,
less more (0) tip