On Sat, 31 Aug 2013, Lawrence Paulson wrote:
It doesn't always work in the panel either. Some lurking bugs maybe.
Can you be more specific? The word bug has no meaning at all.
The sledgehammer panel has had only 1-2 rounds of refinements so far, and
more precise observations by testers on
On Sat, 31 Aug 2013, Christian Sternagel wrote:
Assuming that the grayish background highlighting really indicates
prover activity in the background
This is outdated_color (RGB=EEE3E3 by default). It means that the
asynchronous protocol is in an intermediate state where the editor has no
On Fri, 30 Aug 2013, Makarius wrote:
These days a numpad is relatively rare on keyboards. (I have one at the
big laptop at home, but it has quite different behaviour than the more
regular numpads on old-style stand-alone keyboards.)
I have made some quick tests with my Sony Vaio at home,
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 observations:
- When clicking on the generated
On Tue, 13 Aug 2013, Andreas Lochbihler wrote:
I get the error Attempt to perform non-trivial merge of theories when
I include a bundle from another theory and there are at least two
imports. In the attachment, there's an example.
This should work in Isabelle/ef65d5ee60cf. Are there any
I have also noticed the first issue you mention.
Regarding your other points, a) seems logical to me (you have made your
choice), while b) possibly simplifies the implementation significantly
(otherwise you need to remember to replace the previous choice rather than to
append the text), and it
Hi Makarius,
The error has already gone away in cb82606b8215 when Ondřej moved all the Quotient_...
theories to Main, i.e., there was no non-trivial merge necessary any more. My concrete
application works as expected at the moment.
Andreas
On 02/09/13 12:56, Makarius wrote:
On Tue, 13 Aug
Am 02/09/2013 13:13, schrieb Lawrence Paulson:
I have also noticed the first issue you mention.
Regarding your other points, a) seems logical to me (you have made your
choice), while b) possibly simplifies the implementation significantly
(otherwise you need to remember to replace the
Two months ago, Florian replaced code_module with code_identifier (6646bb548c6b). Now, I
am having trouble using the greater capabilities of code_identifier. I would like to
assign a constant to a different module, say
code_identifier constant replicate \rightharpoonup (SML) My_Module.rep
The French summer vacation period has ended, so I've switched myself now
into consolidation mode to put things into shape for release.
The first release candidates of Isabelle2013-1 will probably happen in the
first or second week of October.
Makarius
For uniformity I almost always use = and would not like to see it printed as
--.
Tobias
Am 02/09/2013 16:24, schrieb Makarius:
(This is just a side-track on HOL notation, which came to me when cleaning up
theories with old ASCII replacement syntax like | -- - Un Int etc. --
which
is very
The earlier the better because, as I told you at ITP, I have a course starting
in the middle of October and they need to use a new Isabelle, in the worst case
a release candidate.
Tobias
Am 02/09/2013 15:37, schrieb Makarius:
The French summer vacation period has ended, so I've switched myself
On Mon, 2 Sep 2013, Lawrence Paulson wrote:
I tend to use -, but I'm afraid I don't know what a print mode is.
A print mode allows to change the way how the system prints things; there
are command line options -m MODE or Isabelle settings to various isabelle
tools for that.
Sometimes
On Mon, 2 Sep 2013, Makarius wrote:
I find myself using the iff notation most of the time to make theories
look nice.
Are there clubs of iff vs. non-iff? If almost everybody is a member of
the iff club we could just remove that print mode.
I've forgotten to point out the relationship to
To me, the ability to use = (on booleans) as an alternative to - is an
artefact of HOL, rather than something to encourage. Almost always, - is more
readable. At least that's my view.
Larry
On 2 Sep 2013, at 19:42, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
Are there
On Mon, 2 Sep 2013, Makarius wrote:
In Isabelle2013 the completion popup was not triggered when deleting
characters (with backspace). Now this is the case and it seems to cause
more frequent hangs for me (since deleting is typically done very fast). Is
this behavior intentional, and if yes,
On 03/09/2013, at 12:24 AM, Makarius makar...@sketis.net wrote:
Are there clubs of iff vs. non-iff? If almost everybody is a member of
the iff club we could just remove that print mode. (We don't have to
consider that for the coming release, to avoid any real-time pressure on this
Same here. - cheers chris
Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote:
Are there clubs of iff vs. non-iff? If almost everybody is a member
of the iff club we could just remove that print mode. (We don't have
to consider that for the coming release, to avoid any
On 09/02/2013 06:30 PM, Makarius wrote:
On Sat, 31 Aug 2013, Christian Sternagel wrote:
First note that for me keyboard input to Isabelle/jEdit typically
hangs every 10 minutes or so, depending on how fast I type (but this
is an old and known issue).
I was hoping that it would have
19 matches
Mail list logo
