| changeset 69204 | d5ab1636660b |
| parent 61609 | 77b453bd616f |
| child 69593 | 3dda49e08b9d |
--- a/src/HOL/Tools/SMT/z3_real.ML Sun Oct 28 16:31:13 2018 +0100 +++ b/src/HOL/Tools/SMT/z3_real.ML Tue Oct 30 16:24:01 2018 +0100 @@ -27,6 +27,6 @@ val _ = Theory.setup (Context.theory_map ( SMTLIB_Proof.add_type_parser real_type_parser #> SMTLIB_Proof.add_term_parser real_term_parser #> - Z3_Replay_Methods.add_arith_abstracter abstract)) + SMT_Replay_Methods.add_arith_abstracter abstract)) end;