Hi Johannes,
Note that emails are typically written in English on this mailing list.
Isabelle uses Z3 to find proofs for goals that are formulated by users. The
query to Z3 is generated by Isabelle. The UNSAT answer from Z3, i.e., the proof
trace, is parsed by Isabelle, which then tries to
Sehr geehrtes Isabelle-Team,
ich beschäftige mich zur Zeit mit dem SMT-Solver Z3 und bin auf ein paar
Paper ihrer Gruppe zum Thema Proof Reconstruction in Z3 gestoßen.
Nun habe ich Isabelle installiert und etwas damit rumgespielt, kann aber
nicht herausfinden, wie ich einen UNSAT-Proof von
