[isabelle-dev] Status of HOL/Library/Old_SMT.thy

[Makarius]

What is the status of HOL/Library/Old_SMT.thy?

I have come across HOL/Library/Old_SMT.thy and the "old_smt" proof
method while disentangling the HOL-Word vs. HOL-Library sessions a
little (6920b1885eff, 0f61ea70d384, f3ad26c4b2d9).

The NEWS entry for Isabelle2015 (May 2015) says:

  - The old 'smt' method has been renamed 'old_smt' and moved to
    'src/HOL/Library/Old_SMT.thy'. It is provided for compatibility,
    until applications have been ported to use the new 'smt' method. For
    the method to work, an older version of Z3 (e.g. Z3 3.2 or 4.0) must
    be installed, and the environment variable "OLD_Z3_SOLVER" must
    point to it.

I did not find any remaining uses of "old_smt" in the visible universe
(Isabelle/f3ad26c4b2d9 + AFP/1cbc172afd56), so it looks like it could be
deleted now. It has been present in two official Isabelle releases with
legacy status, which is normally sufficient.

Note that the next release is anticipated for November/December 2016.
The current Isabelle2016 (February 2016) release already feels a bit old
to me, whenever I need to switch back to it (mainly due to
Isabelle/PIDE/ML changes).


	Makarius