src/HOL/SMT/Examples/cert/z3_bv_arith_06.proof
author boehmes
Tue, 20 Oct 2009 10:11:30 +0200
changeset 33010 39f73a59e855
permissions -rw-r--r--
added proof reconstructon for Z3, added certificates for simpler re-checking of proofs (no need to invoke external solvers), added examples and certificates for all examples, removed Unsynchronized.ref (in smt_normalize.ML)

unsat