Almost always I use <-->. The only exception being a comparison of
booleans, like in "if (a::bool) = b then ..."
-- Peter
On Di, 2013-09-03 at 09:33 +0900, Christian Sternagel wrote:
> Same here. - cheers chris
>
> Florian Haftmann wrote:
>
> >> Are there clubs of "iff" vs. "non-iff"? If alm
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 disappeare
Same here. - cheers chris
Florian Haftmann 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 question
On 03/09/2013, at 12:24 AM, Makarius 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
> question.)
I l
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, wh
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
wrote:
>> Are there clubs of "iff" vs. "non-iff"? If al
> 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 question.)
I am definitely a member of the iff-club. Partly for
On Mon, 2 Sep 2013, Tobias Nipkow wrote:
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.
I have taken that into account. They will get RC1 or RC2, which will be
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 relation
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 pri
I tend to use <->, but I'm afraid I don't know what a print mode is.
Larry
On 2 Sep 2013, at 15:29, Tobias Nipkow wrote:
> 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
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
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
(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 easy with explicit C+b completion in Isabelle/jEdit.)
Isabelle/4379d46c8e13 (Oct 2005) introduces "alternative iff syntax for
e
On Mon, 2 Sep 2013, Tobias Nipkow wrote:
But you are right, this could lead to complications in the
implementation.
At the moment we can ignore questions about "implementation", it is done
quite differently anyway from what one might expect. The sledgehammer
dialog box appears to look like
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
__
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 \ (SML) "My_Module.rep"
Then, code gener
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
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 2
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
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 re
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 genera
I am forwarding this old mail by some robot at Oracle here, since the
issue of "triplication of COMMAND PLUS key events on Mac OS X" was
discussed occasionally on the mailing list.
This includes the meta-question if it makes sense to feed the tracker of
that huge and unmovable company. So far
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, wit
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
co
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 disappeared altogether. So far the
speculation w
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
27 matches
Mail list logo
