src/HOL/SMT/Examples/cert/z3_linarith_03.proof

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)

#2 := false
#7 := 4::int
#5 := 1::int
#4 := 3::int
#6 := (+ 3::int 1::int)
#8 := (= #6 4::int)
#9 := (not #8)
#39 := (iff #9 false)
#1 := true
#34 := (not true)
#37 := (iff #34 false)
#38 := [rewrite]: #37
#35 := (iff #9 #34)
#32 := (iff #8 true)
#27 := (= 4::int 4::int)
#30 := (iff #27 true)
#31 := [rewrite]: #30
#28 := (iff #8 #27)
#26 := [rewrite]: #8
#29 := [monotonicity #26]: #28
#33 := [trans #29 #31]: #32
#36 := [monotonicity #33]: #35
#40 := [trans #36 #38]: #39
#25 := [asserted]: #9
[mp #25 #40]: false
unsat