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