[isabelle-dev] smt2

[Makarius]

On Fri, 14 Mar 2014, Jasmin Christian Blanchette wrote:

>> So far the development has taken place in a private repository. I will 
>> move it to Isabelle next week (in "src/HOL/Tools/SMT2", in session 
>> "HOL-SMT2"). To be able to connect it with Sledgehammer's Isar proof 
>> generator, the best would be to make it part of the "HOL" session, but 
>> that's for a bit later.

This looks very interesting.  I've browsed through it briefly in the web 
presantion of the repository -- I am presently still trying to get back on 
the main track, struggling with global vs. local facts name spaces and 
related performance problems.

We have recently seen much increase of size and facilities in main HOL, 
but resources are always finite.  Just as a habit, one needs to remove old 
things occasionally.

While experimenting with the increasingly useful Isabelle/ML IDE, I've 
found various spots that are awaiting further cleanup, renovation or 
demolition. Just some arbitrary examples:

   * HOL/SAT.thy with some related ML modules.  I've brushed this up
     recently, e.g. to get module names vs. file names right.  Actual
     external SAT solvers don't work, though, so it is not really usable.

     A candidate for HOL-ex?

   * HOL/Tools/choice_specification.ML which is loaded into
     HOL/Hilbert_Choice.thy -- really old stuff that would require serious
     renovation if actually used: 'ax_specification' with its unchecked
     axiomatization is actually unsed, and 'specification' only by
     HOL-Auth (and its many clones).

     A candidate for HOL-Library, after removing the axiomatic part?
     Nitpick seems to have special tricks to cope with it, though.


 	Makarius