src/HOL/SMT/Examples/cert/z3_linarith_18.proof
Thu, 05 Nov 2009 15:24:49 +0100 boehmes handle let expressions inside terms by unfolding (instead of raising an exception),
less more (0) tip