My changes to Complete Distributive Lattices are now integrated in the
development version of Isabelle.
I want to thank Manuel Eberl for helping with testing and pushing the
update into repository.
Viorel Preoteasa
On Fri, Mar 9, 2018 at 12:48 PM, Lawrence Paulson <l...@cam.ac.uk> wrote
Aug 2017, at 15:59, Viorel Preoteasa <viorel.preote...@aalto.fi
<mailto:viorel.preote...@aalto.fi>> wrote:
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
OK, I understand, what is the time frame for going back to normal? I did
spent some time on this and I would like to see it finished.
As I mentioned earlier, I added finite lattices to simplify the proofs
in Enum.thy that finite_n are distributive complete lattices. However,
searching for
, at 15:59, Viorel Preoteasa <viorel.preote...@aalto.fi
<mailto:viorel.preote...@aalto.fi>> wrote:
There is also AFP. If there are instantiations of
complete_distrib_lattice, then most probably they will fail.
One simple solution in this case could be to keep
of
complete_distrib_lattice, then most probably they will fail.
One simple solution in this case could be to keep also the
old complete_distrib_lattice as complete_pseudo_distrib_lattice.
Viorel
On 8/26/2017 3:06 PM, Lawrence Paulson wrote:
On 25 Aug 2017, at 20:14, Viorel Preoteasa <viorel.pre
be fine if someone is willing to undertake it
before the RC stabilization phase.
Cheers,
Florian
Am 24.08.2017 um 00:42 schrieb Lawrence Paulson:
Sounds good to me. Can anybody think of an objection?
Larry
On 23 Aug 2017, at 15:17, Viorel Preoteasa <viorel.preote...@aalto
is accepted as a filter, then one could have a complete lattice
of filters (filter will be closed to arbitrary intersections). But I
don't know
if this complete lattice is distributive.
Viorel
On 2017-08-24 20:54, Viorel Preoteasa wrote:
I have now a file with the new class, and all
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
Hi,
I managed to get it working with the latest version of jedit_build.
However, I could only get it using scala-2.8.2.final and not with
scala-2.9.1-1.
Using scala-2.9.1-1 on OS X Lion generates the error:
### Building Isabelle/jEdit ...
4:18:55 PM [main] [error] PluginJAR: Error while
Hello,
I am trying to use jedit with the Isabelle development version
I have scala-2.9.1-1 and I downloaded jedit_build-20120313.
I set the paths
export
SCALA_HOME=/Users/viorel/Work/isabelle-dev/isabelle/contrib/scala-2.9.1-1
export
On 3/27/12 11:59 PM, Makarius wrote:
On Tue, 27 Mar 2012, Viorel Preoteasa wrote:
I am trying to use jedit with the Isabelle development version
I have scala-2.9.1-1 and I downloaded jedit_build-20120313.
I set the paths
export
SCALA_HOME=/Users/viorel/Work/isabelle-dev/isabelle/contrib
11 matches
Mail list logo
