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
Dear list,
maybe the following results about "lex" are worthwhile to add to the
library?
lemma lex_append_right:
"(xs, ys) ∈ lex r ⟹ length vs = length us ⟹ (xs @ us, ys @ vs) ∈ lex r"
by (force simp: lex_def lexn_conv)
lemma lex_append_left:
"(ys, zs) ∈ lex r ⟹ (xs @ ys, xs @ zs) ∈ lex r"
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
