I have been very busy, but I will find time to work on it.
Viorel
On 11/23/2017 6:46 PM, Lawrence Paulson wrote:
Whatever happened with this? The new release has been out for a while,
and it would make sense to integrate your work now, well before any
thought of a new release.
Larry
On 27 A
Whatever happened with this? The new release has been out for a while, and it
would make sense to integrate your work now, well before any thought of a new
release.
Larry
> On 27 Aug 2017, at 15:59, Viorel Preoteasa wrote:
>
> I managed to integrate the new complete distributive lattice into H
This is a brief summary of the current situation:
* The current RC version is
http://isabelle.in.tum.de/website-Isabelle2017-RC3 and
http://isabelle.in.tum.de/website-Isabelle2017 is an alias for that.
* http://isabelle.in.tum.de/repos/isabelle/rev/ebb97a834338 is a
preliminary merge of the isabe
> My plan would be to fork the AFP 2017 release branch tomorrow (around
> midnight CET from Mon to Tue).
>
> There still seems to be quite a bit of ongoing activity - if there is
> anything that needs to go into the afp-2017 release, please let me know.
One more thing that is of interest to use
My plan would be to fork the AFP 2017 release branch tomorrow (around midnight
CET from Mon to Tue).
There still seems to be quite a bit of ongoing activity - if there is anything
that needs to go into the afp-2017 release, please let me know.
Cheers,
Gerwin
> On 9 Sep 2017, at 04:30, Makari
We are now past the fork point for the Isabelle2017 release.
Here is a summary of the status of the Isabelle development process:
* https://bitbucket.org/isabelle_project/isabelle-release/ is where
the final release preparations happen before roll-out in a few
weeks.
The st
On 08/09/17 11:13, Makarius wrote:
> The all-important release fork will happen today in the evening.
That is now!
Within the next hour there should not be any pushes to
http://isabelle.in.tum.de/repos/isabelle in order to avoid confusion
about the two branches.
I will come back a bit later wit
On 03/09/17 12:06, Makarius wrote:
>
> The isabelle-dev repository remains open for 3 more days. Afterwards it
> forks to https://bitbucket.org/isabelle_project/isabelle-release and
> further changes (really important ones!) need to be sent to me via email.
There were some delays, but we are now
Dear Florian,
thanks for the explanation and the hint on style.
The below pattern works perfectly in our formalization.
Cheers,
René
> Am 31.08.2017 um 14:03 schrieb Florian Haftmann
> :
>
> Note that the pattern above is avoided nowadays by an interpretation
> with mixin definitions:
>
> lo
On 21/08/17 20:24, Makarius wrote:
>
> The first official release candidate Isabelle2017-RC1 is anticipated for
> 2/3-Sep-2017, that is a bit less than 2 weeks from now.
>
> That is also the deadline for any significant additions.
That is today. I will publish Isabelle2017-RC1 within a few hours
Hi Rene,
> =
> locale foo = fixes f :: "nat => nat"
> assumes f_mono[termination_simp]: "f x <= x"
> begin
>
> fun bar :: "nat => nat" where
> "bar 0 = 0"
> | "bar (Suc x) = Suc (bar (f x))"
>
> end
>
> definition com where
> [code del]: "com = foo.bar id"
>
> interpretation foo id
>
On 24/08/17 09:38, Thiemann, Rene wrote:
>
> - Most changes have been caused by integrating session-qualified theory
> imports.
> This will also require a reform of the splitting of sessions, which
> previously
> was structured towards a fast build-process, but now should be structured
> mo
On 24/08/17 17:40, Florian Haftmann wrote:
>
> Hence that change should be fine if someone is willing to undertake it
> before the RC stabilization phase.
We are already in stabilization phase for some weeks. There are a few
days left until Isabelle2017-RC1 (presumably on 03-Sep-2017) to make
sma
Dear Florian,
>> - There have been some changes w.r.t. code-generation which now lead
>> to runtime exception in the generated code. For instance, now
>> I get code like
>> “f x = Code.abort …”
>> whereas in 2016-1 there was a proper code like
>> “f x = some ordinary right-hand side”
>> We d
On 8/27/2017 6:11 PM, Lawrence Paulson wrote:
In the AFP, grep picks up these:
~/isabelle/afp/devel/thys: grep -l complete_distrib_lattice -r .
./Coinductive/Examples/CCPO_Topology.thy
./Concurrent_Ref_Alg/Refinement_Lattice.thy
./DataRefinementIBP/Diagram.thy
./DataRefinementIBP/Hoare.thy
./D
Hi Viorel,
it's probably easiest to send a patch containing your changes to this mailing
list. (Alternatively, a copy of all the files you changed.) Some Isabelle
committer can then push this to the testboard which will run the whole AFP.
Cheers
Lars
On 27 August 2017 16:59:44 CEST, Viorel Pre
In the AFP, grep picks up these:
~/isabelle/afp/devel/thys: grep -l complete_distrib_lattice -r .
./Coinductive/Examples/CCPO_Topology.thy
./Concurrent_Ref_Alg/Refinement_Lattice.thy
./DataRefinementIBP/Diagram.thy
./DataRefinementIBP/Hoare.thy
./DataRefinementIBP/Statements.thy
./LatticePropertie
I managed to integrate the new complete distributive lattice into HOL
library.
The changes are these:
Complete_Lattice.thy
- replaced the complete_distrib_lattice with the new stronger version.
- moved some proofs about complete_distrib_lattice and some
instantiations to Hilbert_Choice
Hil
> On 25 Aug 2017, at 20:14, Viorel Preoteasa wrote:
>
> One possible solution:
>
> Add the new class in Complete_Lattice.thy, replacing the existing class
>
> Prove the instantiations and the complete_linearord subclass later
> in Hilbert_Choice.
>
> On the other hand, it seems inconvenient to
I have investigated the possibility of replacing the existing
complete_distrib_lattice with the stronger version.
Here are the problems:
1. The new class needs Hilbert choice in few places: proving the dual
of the distributivity property, proving the set and fun instantiations,
and proving that
On 2017-08-24 23:25, Manuel Eberl wrote:
Purely out of interest: Does this also hold for filters?
Manuel
Do filters form a complete lattice? It seems that a filter of a lattice
should be nonempty.
I think that this condition would prevent the set of filters to be a
lattice.
If empty set
Am 24.08.2017 um 22:39 schrieb Manuel Eberl:
> On 2017-08-24 17:34, Florian Haftmann wrote:
>> I would still appreciate if someone would take the comment »Deviates
>> from the definition given in the library in number theory« as a starting
>> point to reconcile that definition with src/HOL/Number_T
For the final record:
> \phi is the result of a simple typo accident
see http://isabelle.in.tum.de/repos/isabelle/rev/ba94aeb02fbc
> Concerning \mu and \nu, I am currently investigating whether an import
> swap could re-establish the situation known from Isabelle2016-1
see http://isabelle.in.tum
On 2017-08-24 17:34, Florian Haftmann wrote:
> I would still appreciate if someone would take the comment »Deviates
> from the definition given in the library in number theory« as a starting
> point to reconcile that definition with src/HOL/Number_Theory/Totient.thy.
Oh actually I fixed that a few
Purely out of interest: Does this also hold for filters?
Manuel
On 2017-08-24 20:54, Viorel Preoteasa wrote:
> I have now a file with the new class, and all necessary proofs
> (both distributivity equalities, bool, set, fun interpretations,
> proofs of the old distributivity properties).
>
> I
I have now a file with the new class, and all necessary proofs
(both distributivity equalities, bool, set, fun interpretations,
proofs of the old distributivity properties).
I have also the proof that complete linear order is subclass of
the new complete distributive lattice class.
Are there any
As far as I remember, I introduced the complete_distrib_lattice class
after realizing the a complete lattice whose binary operations are
distributive is not necessarily a distributive complete lattice. Hence
the specification of that type class has been contrieved without
consulting literature.
H
Hi Rene,
> - In the NEWS I read about freeing short constant names like the
> “Renamed ii to imaginary_unit in order to free up ii as a variable”.
> I definitely support this kind of change, but at the same time found
> quite the opposite in HOL-Algebra:
> If one imports HOL-Algebra.Multip
Dear all,
let me share my opinions after porting IsaFoR to yesterdays development version:
- In total the transition from our 2016-1 source went quite smooth
(~ 14 hours for whole of IsaFoR)
- Most changes have been caused by integrating session-qualified theory imports.
This will also requ
Sounds good to me. Can anybody think of an objection?
Larry
> On 23 Aug 2017, at 15:17, Viorel Preoteasa wrote:
>
> Hello,
>
> I am not sure if this is the right place to post this message, but it is
> related to the upcoming release as I am prosing adding something
> to the Isabelle library.
Hello,
I am not sure if this is the right place to post this message, but it is
related to the upcoming release as I am prosing adding something
to the Isabelle library.
While working with complete distributive lattices, I noticed that
the Isabelle class complete_distrib_lattice is weaker compa
Dear Isabelle contributors,
we are now definitely heading towards the Isabelle2017 release.
The first official release candidate Isabelle2017-RC1 is anticipated for
2/3-Sep-2017, that is a bit less than 2 weeks from now.
That is also the deadline for any significant additions.
I have already u
32 matches
Mail list logo