Hi Larry,
Am 15.03.2014 um 16:27 schrieb Lawrence Paulson l...@cam.ac.uk:
But working very well, in my experience.
I'm glad to hear that. :)
Now, will smt2 calls be suitable for the Library and AFP?
No, because they suffer from the exact same issues as smt calls. We could of
course rethink
On Sat, 15 Mar 2014, Lawrence Paulson wrote:
Now, will smt2 calls be suitable for the Library and AFP?
As far as I can tell the license did not change: Z3 is non-free in the
sense of educational / non-commercial use only. This means libraries that
critically depend on Z3 would de-facto
But working very well, in my experience.
Now, will smt2 calls be suitable for the Library and AFP?
Larry
On 6 Mar 2014, at 15:43, Jasmin Christian Blanchette
jasmin.blanche...@gmail.com wrote:
As you may know, Sascha and I have been working on a new version of the smt
proof method, called
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
Hi Makarius,
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
Hi Jasmin,
On 14/03/14 14:18, Jasmin Blanchette wrote:
Another candidate is Quickcheck_Narrowing.thy. Nothing in HOL seems to
depend on it, and (please correct me if I'm mistaken) hardly anybody go into the trouble of setting
up Quickcheck (and GHC) so that it uses the narrowing strategy.
I
Hi Andreas,
Am 14.03.2014 um 15:26 schrieb Andreas Lochbihler
andreas.lochbih...@inf.ethz.ch:
On 14/03/14 14:18, Jasmin Blanchette wrote:
Another candidate is Quickcheck_Narrowing.thy. Nothing in HOL seems to
depend on it, and (please correct me if I'm mistaken) hardly anybody go into
the
On Fri, 14 Mar 2014, Andreas Lochbihler wrote:
To make one's type work with narrowing, however, is hardly documented.
Recently, I finally got around to provide narrowing generators for
Coinductive in the AFP (AFP/1fffd2ebbd28), but I had to study all the
implementation of the narrowing engine
Hi Jasmin,
On 14/03/14 16:05, Jasmin Blanchette wrote:
Hi Andreas,
Am 14.03.2014 um 15:26 schrieb Andreas Lochbihler
andreas.lochbih...@inf.ethz.ch:
On 14/03/14 14:18, Jasmin Blanchette wrote:
Another candidate is Quickcheck_Narrowing.thy. Nothing in HOL seems to
depend on it, and
On Fri, 14 Mar 2014, Andreas Lochbihler wrote:
IIRC, the AFP policy is (was?) that all entries that import at least one
theory from HOL-Library are based on HOL-Library.
I can't speak for the AFP editors, but that might be just some
old-fashioned custom. In general it does not even work
Hi Andreas,
How big an issue is it to you if we move narrowing to Library?
[...] If you do so, please make sure that the connection to the datatype
packages is kept, i.e., narrowing generators are generated for all datatypes
(even those that are defined while narrowing was not in scope).
On 15.03.2014, at 2:39 am, Makarius makar...@sketis.net wrote:
On Fri, 14 Mar 2014, Andreas Lochbihler wrote:
IIRC, the AFP policy is (was?) that all entries that import at least one
theory from HOL-Library are based on HOL-Library.
I can't speak for the AFP editors, but that might be
Hi all,
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
Hi all,
As you may know, Sascha and I have been working on a new version of the smt
proof method, called smt2. It is effectively a clone of smt, but with the
Z3 interaction (problem generation, proof parsing, and reconstruction)
rewritten from scratch, with the following short-term goals:
1.
14 matches
Mail list logo
