Hallo,
being beginner in Isabelle, you may safely ignore this post.
AFAIU {..deliver wrong positive.
AFAIK the questionif 0 is part of natural numbers is disputed. Was there
some solution in recent years?
Depending on that {1..
Florian,
The whole setup has grown over time and initially I may h
Florian,
The whole setup has grown over time and initially I may have preferred {..just like you did. I would welcome your proposed changes.
I agree, sums look nicer with {..clearly shows that the set/sum is bounded, something that is otherwise implicit
in the type.
Tobias
On 04/07/2016 21:
> Another way of getting simultaneous tests would be to use subrepos. I.e.
>
> test-repo/
>isabelle/ (subrepo)
>afp/ (subrepo)
>
> The trigger would then be the push to test-repo, not to any of the subrepos,
> and you would get a predictable combination as well.
Right, that's one
Another way of getting simultaneous tests would be to use subrepos. I.e.
test-repo/
isabelle/ (subrepo)
afp/ (subrepo)
The trigger would then be the push to test-repo, not to any of the subrepos,
and you would get a predictable combination as well.
Cheers,
Gerwin
> On 5 Jul 2016, a
> The problem I was referring to is that in order to get a deeper idea
> what's going on you want to have a look at the topology of the history.
> However I guess this is closely related to my surprise that not both
> patches to distro and AFP pushed in proximity have been considered as
> one buil
>> This is currently not implemented. Isabelle testboard will always use
>> AFP devel and vice versa. It is not possible to test Isabelle testboard
>> and AFP testboard together.
>
> But I regard this as a central use case: if a change to the distro
> demands changes in the AFP, you want to test t
* Proof method "blast" is more robust wrt. corner cases of Pure
statements without object-logic judgment.
This refers to Isabelle/8bbd325e89e6, the relevant changes are by Larry
(9a2377b96ffd, d2d26ff708d7).
Makarius
___
isabelle-dev mailing l
* The defining position of a literal fact ‹prop› is maintained more
carefully, and made accessible as hyperlink in the Prover IDE.
* Commands 'finally' and 'ultimately' used to expose the result as
literal fact: this accidental behaviour has been discontinued. Rare
INCOMPATIBILITY, use more explic
Hi all,
see 59803048b0e8 for some basic facts about almost everywhere bijections
aka permutations. Maybe this will become a convenient coagulation point
for various scattered material in the future.
It turned out quite ambitious to formulate basic properties, e.g.
circularity. I d
Hi all,
in 1a474286f315 I have introduced a locale for (total) bijections,
allowing to obtain typical facts like ‹inv f ∘ f = id› by interpretation.
The motivation was that most of these facts have not ‹bij› but ‹inj› or
‹surj› as premise, which makes proof complicated due to two lifting
>> 3. Go to https://ci.isabelle.systems/jenkins/job/testboard-afp/ and
>> await new build run to be scheduled.
>
> There can currently only be one testboard build running at a time. That
> means you should wait to push until the previous run is finished.
>
> I understand that this is not ideal. I
>> 1. Changesets to dist and AFP exist as hg patches.
>
> This is currently not implemented. Isabelle testboard will always use
> AFP devel and vice versa. It is not possible to test Isabelle testboard
> and AFP testboard together.
But I regard this as a central use case: if a change to the distr
> The problem with {.. every lemma involving {m.. {.. all problems: not all proof methods invoke simp all the time.
>
> I consider {.. gains very little by using it. One could even think aout replacing it by
> {0..n. n ^ 3) {0..\n =
0..
term "setsum (\n. n ^ 3) {..\n
term "setsum (\n. n ^ 3) {0..m
To add to my last mail:
> 3. Go to https://ci.isabelle.systems/jenkins/job/testboard-afp/ and
> await new build run to be scheduled.
There can currently only be one testboard build running at a time. That
means you should wait to push until the previous run is finished.
I understand that this is
Hi Johannes,
the multiset ordering (contrary to the subset ordering) does not have this
property:
lemma "{#0#} <= {#Suc 0#}”
unfolding Multiset_Order.le_multiset⇩H⇩O by auto
(the actual notation is #⊆# and not <=).
I tried locally to apply the changes of my previous email t
Hi Mathias,
there is at least the type class 'canonically_ordered_monoid' which has
the property a <= b <--> ?c. a + c = b which implies 0 <= a for all a.
Are the multisets already in this typeclass?
- Johannes
Am Dienstag, den 28.06.2016, 10:04 +0100 schrieb Mathias Fleury:
> Dear type-classe
Yes I second that. It surely is a good idea to just use it only as a
input translation.
- Johannes
Am Samstag, den 02.07.2016, 21:08 +0200 schrieb Florian Haftmann:
> Hi all,
>
> since cf26dd7395e4, ‹surj f› is a mere abbreviation for ‹range f =
> UNIV›. This is a little bit unfortunate s
17 matches
Mail list logo
