Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] HOL-Analysis changes: Incomplete NEWS

Email Gateway (Jun 22 2026 at 10:57):

From: Fabian Huch <huch@in.tum.de>

In HOL-Analysis, 'det' refers to a different constant now, but I didn't
find any NEWS about that.

Fabian

Email Gateway (Jun 22 2026 at 11:05):

From: Manuel Eberl <manuel@pruvisto.org>

This is based on some material from me. I think Larry was the one to
actually put it in the distribution a while ago.

I think I actually intended for this to be used by writing "eucl.det"
(since it comes from an interpretation of the
finite_dimensional_vector_space locale with the prefix "eucl"), but
apparently that interpretation is (and always has been) made in
HOL-Analysis with a "?" modifier, so "det" also works without the prefix.

Still, this is probably an acceptable state of affairs all in all. I'll
update the NEWS file in that regard.

Manuel

On 6/22/26 12:57, Fabian Huch wrote:

In HOL-Analysis, 'det' refers to a different constant now, but I
didn't find any NEWS about that.

Fabian

Email Gateway (Jun 22 2026 at 11:06):

From: Lawrence Paulson <lp15@cam.ac.uk>

It’s this:

• Session "HOL-Analysis": much new material including Bounded_Variation,
  Rectifiable_Paths and Absolute_Continuity. Change_Of_Vars has been
  generalised to Euclidean spaces. Stronger versions of the FTC, now for
  countable rather than finite sets. Minor INCOMPATIBILITY

So in particular, unqualified det is now eucl.det rather than matrix_det (which is Determinants.det). Maybe hide_const (open) is the answer?

Larry

On 22 Jun 2026, at 11:57, Fabian Huch <huch@in.tum.de> wrote:

In HOL-Analysis, 'det' refers to a different constant now, but I didn't find any NEWS about that.

Last updated: Jul 02 2026 at 07:34 UTC