On 2017-07-05 22:09, Manuel Eberl wrote:
> I still want to take care of two really tiny things: […] and the proper
> printing
> of "nat" values as numerals instead of successor notation.
This is now done as of adf3155c57e2. I should note that I was somewhat
imprecise, by ‘printing of "nat"
I’ve been using it a bit and it’s pretty useful! Thanks
Larry
> On 9 Jul 2017, at 17:16, Fabian Immler wrote:
>
> A while ago, Florian Haftmann sent a command that does something like this to
> the mailing list [1]. I attach a version that works with current
> Isabelle2016-1
A while ago, Florian Haftmann sent a command that does something like this to
the mailing list [1]. I attach a version that works with current Isabelle2016-1
(not sure if I got all the modifications right, but it seems to work at least
on the example in the .thy file).
Fabian
[1]
I currently supervise a student who's investigating proof refactoring. One
possible outcome of this would be a tool that also does what you suggested.
It's a little too early to tell, though.
Cheers
Lars
On 8 July 2017 23:28:42 CEST, Lawrence Paulson wrote:
>No, that’s
No, that’s precisely what I’d like to avoid. I prefer texts that you can
actually read. It would be great to have something automatically generated,
even if it needed manual tweaking (e.g. to rename variables).
And I’ve gone to some effort purging instances of “guess” from existing proofs.
I am always using the new auto-complete facility for
proof (cases “...”)
and for induction. But could this be done for “proof" with any method, simply
copying out the states of the subgoals? Then people would make a lot less use
of “subgoals”, etc.
Larry
> On 5 Jul 2017, at 21:04,
Hi Makarius,
> Is there anything else to take into account for this late-summer release
> process?
Simon Cruanes (cc:) and I are still working on Nunchaku, which we intend to
become Nitpick's successor. I have some patches locally that move the current
"Nunchaku.thy" to Main (it's not much
Nothing fancy, just a couple of code_post rules to rewrite successor
notation into numeral notation after evaluation and before printing. I
don't know if there's a better way to do that, but I think we discussed
this on the mailing list a while ago and came to the conclusion that
code_post is
What’s the idea here?
Larry
> On 5 Jul 2017, at 21:09, Manuel Eberl wrote:
>
> the proper printing of "nat" values as numerals instead of successor notation.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
I still want to take care of two really tiny things: the "subseq"
situation and the proper printing of "nat" values as numerals instead of
successor notation.
Just mentioning that for the sake of completeness.
Manuel
On 2017-07-05 21:04, Makarius wrote:
> Dear all,
>
> we are now almost 7
Dear all,
we are now almost 7 months after Isabelle2016-1 (December 2016).
Following the standard schedule, the Isabelle2017 release should appear
at the start of October 2017.
During the last 3 weeks in July, I will be in Cambridge. That is also a
possibility to show me old and new problems in
Dear all,
this is the last call for small amendments and finalization on the main
Isabelle repository.
Unless there are any last-minute surprises, the fork for Isabelle2013-1
will happen Thu 03-Oct-2013.
This means the history of the official release will continue on
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 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
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
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
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
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 08/17/2013 04:05 PM, Makarius wrote:
in the past few weeks the coming release has been mentioned in passing
several times. So far the precise schedule is not clear, but just from
the distance to Isabelle2013 and the amount of material that is about to
be finished for Isabelle2013-1, it has
So the time to point out further issues or pending projects is now --
apart from the well-known HOL-BNF and PIDE improvements that are already
underway. In general there is no reason to rush anything on any
particular release train, since they are rather frequent anyway. A
release is a
Dear all,
in the past few weeks the coming release has been mentioned in passing
several times. So far the precise schedule is not clear, but just from
the distance to Isabelle2013 and the amount of material that is about to
be finished for Isabelle2013-1, it has to be rather soon after the
22 matches
Mail list logo