Am 21/09/2013 03:08, schrieb Alessandro Coglio:
Hello,
The attached file contains a fairly heterogeneous collection of potential
extensions to the Isabelle library, which I've been developing as part of some
projects that I'm working on. I think that other Isabelle users may find them
Am 21/09/2013 03:08, schrieb Alessandro Coglio:
I also have a general question about library vs. AFP. There seem to be clear
cases of things that should go into the library (e.g. new theorems on lists or
sets) and clear cases of things that should go into the AFP (e.g. a theory of
On Mon, 2 Sep 2013, Makarius wrote:
The first release candidates of Isabelle2013-1 will probably happen in
the first or second week of October.
How is the general situation? And especially the situation for HOL-BNF?
Is it feasible to target the first week of October for Isabelle2013-1-RC1?
The first release candidates of Isabelle2013-1 will probably happen in the
first or second week of October.
How is the general situation? And especially the situation for HOL-BNF?
HOL-BNF is a long-term construction yard. There happens to be a lot of
development these days, but it's
On Mon, 16 Sep 2013, Lawrence Paulson wrote:
Any generated metis calls only self-insert if clicked before s/h
terminates. If you ignore your session for a few minutes while s/h runs
(as many people do), then the highlighted links will be inactive when
you get back. I've checked this several
On Mon, 23 Sep 2013, Makarius wrote:
With Isabelle/322a3ff42b33 there is now completion for the history text
field behind it.
It is again one of these typical instances of spending 2h to make it
work on Linux and Windows, and requiring days or weeks to find out why
Apple/Oracle don't quite
On Tue, 24 Sep 2013, Jasmin Christian Blanchette wrote:
As far as HOL-BNF is concerned, you can branch any time. What doesn't
make it in this release will make it into the next one.
OK, I will tell you when we are getting close to the fork point.
Just formally for a proper release, you need
On Mon, 2 Sep 2013, Tobias Nipkow wrote:
Am 02/09/2013 11:18, schrieb Makarius:
The sledgehammer panel has had only 1-2 rounds of refinements so far, and more
precise observations by testers on this mailing list will be required to make it
work smoothly for the coming release.
Some
On Mon, 2 Sep 2013, Lawrence Paulson wrote:
I agree that the generated proof should start on a fresh line, because
these calls are often quite lengthy text strings.
The fresh line is there in Isabelle/88c6e630c15f but it is merely
minimalistic tuning.
The concept that is missing here is some
On Thu, 5 Sep 2013, Florian Haftmann wrote:
I also observed that if you use sledgehammer as old-style keyword, the
proof text is inserted after instead of just replacing
This goes back to Isabelle/a0db255af8c5 from 1 month ago:
sledgehammer sendback always uses Markup.padding_command:
On Thu, 5 Sep 2013, Florian Haftmann wrote:
At some stage I would expect some »click and copy to theory buffer«
functionality, e. g.
thm foo
or
from foo have prop .
I would say that is another instance of structured editing. Output
should provide systematic markup about
Am 24.09.2013 um 22:10 schrieb Makarius makar...@sketis.net:
OK, I will tell you when we are getting close to the fork point.
Thanks. We'll try to maintain the ready to be forked invariant, but it's
always good to have advance notice, if nothing else so that we avoid bigger
changes right
Thanks for the response, but my issue has nothing to do with editing the
surrounding text. On the contrary, it has to do with activating s/h, walking
away from the computer, and coming back to find that sendback does not work.
So I'm force to watch s/h and choose one of the metis calls before
On Thu, 5 Sep 2013, Lars Noschinski wrote:
On 05.09.2013 13:35, Florian Haftmann wrote:
Hi,
after some time playing around with the new sledgehammer panel
(ab4edf89992f), here my feedback:
Regarding this (and also the new Find panel), I would like to see a keyboard
shortcut, not only to
On Tue, 10 Sep 2013, Alfio Martini wrote:
On the other hand, the (propositional) operators of HOL-formulae are
still not properly shown in the sidekick pane as the image attached
shows. I am not sure if this is a feature or a known bug, but this is
problem is also present in the current
On Wed, 11 Sep 2013, Gerwin Klein wrote:
An aside: The more AFP entries are used as proper libraries, the more
we need to think how release processes need to interact etc.
We've been thinking about that from the start. There shouldn't be
anything special to do. AFP-2013-1 will come out a few
On Mon, 16 Sep 2013, Josh Tilles wrote:
On Tue, Jul 30, 2013 at 3:42 PM, Lawrence Paulson l...@cam.ac.uk wrote:
This could be a valuable service, especially for long lists of applys.
Thank you for the encouragement! I'm glad to see you agree.
(A proof like by (induct n) auto should be
On Mon, 16 Sep 2013, Josh Tilles wrote:
Interesting—I had assumed that changing the proof of a lemma and/or
theorem had no functional impact on the code once said lemma/theorem had
been verified. Am I incorrect about that? (If the explanation is
complicated, please don't feel obligated to go
On Tue, 24 Sep 2013, Jasmin Blanchette wrote:
54c8dee1295a should address that.
BTW, Pretty.item allows to make nice square bullets for itemization
(visible in Isabelle/jEdit only).
Do you have a specific use in mind w.r.t. BNF or is this just a general
hint (e.g. for Sledgehammer and
Am 24.09.2013 um 23:43 schrieb Makarius makar...@sketis.net:
This is a question to hard-core users of Mac OS X.
How important is the canonical key sequence COMMAND comma as defined by
Apple?
It's probably important, but I don't use it (for lack of having memorized it).
Alternatively, I
Never tried using this with jEdit.
I won't mind having the Mac cursor-movement keyboard shortcuts.
Larry
On 24 Sep 2013, at 22:43, Makarius makar...@sketis.net wrote:
How important is the canonical key sequence COMMAND comma as defined by
Apple?
Hi all,
Isabelle/jEdit is currently unwilling to process theories (as of dcefe11f28f2).
I open up an existing theory file, e.g.
isabelle jedit -l HOL-BNF src/Doc/Datatypes/Datatypes.thy
The file is correctly opened, but nothing is processed -- no imports are
processed, the theory text has
22 matches
Mail list logo
