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
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
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
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
