more official legacy status;
authorwenzelm
Fri Oct 07 10:46:34 2016 +0200 (2016-10-07)
changeset 640780b22328a353c
parent 64073 cffd5f537206
child 64079 ff26032b7f2a
more official legacy status;
src/HOL/Library/Old_SMT.thy
     1.1 --- a/src/HOL/Library/Old_SMT.thy	Fri Oct 07 10:31:34 2016 +0200
     1.2 +++ b/src/HOL/Library/Old_SMT.thy	Fri Oct 07 10:46:34 2016 +0200
     1.3 @@ -142,7 +142,8 @@
     1.4  method_setup old_smt = \<open>
     1.5    Scan.optional Attrib.thms [] >>
     1.6      (fn thms => fn ctxt =>
     1.7 -      METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts))))
     1.8 +      (legacy_feature "Proof method \"old_smt\" will be discontinued soon -- use \"smt\" instead";
     1.9 +       METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts)))))
    1.10  \<close> "apply an SMT solver to the current goal"
    1.11  
    1.12