can someone please integrate the attached patch which introduces a locale for
I tested the patch by running all sessions of the AFP though without
there have been no problems.
It's the operation identification phase of Autoref,
quite difficult to debug ... I have not yet looked at it due to
I found the culprit:
summary: adapting entries to new Deriving mechanism
in LTL_to_GBA-theory, this removes a linorder-constraint on
there are some changes I would like to add for the upcoming release. It would
be nice, if someone can integrate them:
- improved code equations for binomial coefficients and certain
> I already moved a few small lemmas.
> I also defined the notion of an algebraic number; as soon as your AFP entry
> works with the development version of Isabelle again (is that already the
Yes, it should work. (At least, on Friday afternoon, it worked)
> I added the efficient code equations for fact and binomial, and similar ones
> for pochhammer and gbinomial.
> I also adapted everything from Square_Free_Factorization and
> Missing_Polynomial that seemed to be of general interest to me (especially
> the generalisation of the
>> I’m puzzled. In ~~/src/HOL/Library/Poly_Deriv.thy I found no notion of
>> algebraic number.
> Oh, yes, you're right. It's in
Ah, I see. Indeed:
> I have already some post-release patches in the pipeline which would add
> this instance anyway. So, there is no demand for action here at the moment.
> Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
> thus very hardly different from syntactic classes,
ere is an abstract factorial ring with
> subclass (in factorial_semiring) semiring_gcd
> and hence the possibility to formulate also the other prominent instance
> poly :: (factorial_semiring) factorial_semiring
> This will still take some time however.
in the following theory, the export-code fails:
(Isabelle 957ba35d1338, AFP 618f04bf906f)
definition foo :: "'a :: factorial_semiring_gcd ⇒ 'a ⇒ 'a" where
"foo x y = gcd y
thanks Manuel and Florian for pointing to other variants of discrete
I would like to mention a fairly recent one in
It defines log_floor and log_ceiling :: “int => int => nat”.
The advantage of these functions are improved code
thanks for your efforts, but I believe there is already a more efficient way to
In your implementation, consider your intlog2_aux which roughly requires y
iterations if log2(x) = y,
since you always just add 1 to the accumulator.
For some of my applications this
>> - 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”
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
thanks for the explanation and the hint on style.
The below pattern works perfectly in our formalization.
> Am 31.08.2017 um 14:03 schrieb Florian Haftmann
> Note that the pattern above is avoided nowadays by an
with HMA_Connect you have a bidirectional connection between “‘a^’n’^m” and “‘a
However, when you transfer something from “‘a^’n^’m” to “‘a mat”, then you get
constraint that the dimensions of the matrix must be non-zero.
To be more precise, assume the following
Mail list logo