src/HOL/SMT/Examples/ROOT.ML
2009-11-11 wenzelm 2009-11-11 uniform use of simultabeous use_thys;
2009-10-20 boehmes 2009-10-20 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)