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" values
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 (not sure if I got
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]
http://www.m
What I’m requesting requires no sophistication at all. It is merely to automate
what we currently do by copying from one window and pasting to another, while
inserting “fix”, “assume” and “show” in the obvious places.
Larry
> On 9 Jul 2017, at 16:32, Lars Hupel wrote:
>
> I currently supervise
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 precisely what I’d like
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.
Larr
We already have proof goal_cases. Is that what you mean?Peter Original Message Subject: Re: [isabelle-dev] The coming release of Isabelle2017From: Lawrence Paulson To: Markus Wenzel CC: isabelle-dev I am always using the new auto-complete facility for proof (cases “...”) and for in
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, M
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 code
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 indee
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
https://mailmanbroy.informatik.tu-muench
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 month
12 matches
Mail list logo