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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
