From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>

Dear All,

I am looking for the original conference proceedings/journal articles or

technical reports that describe the following libraries that are available

from the main distribution of Isabelle/HOL:

- Standard mathematics library that is available from Main/Complex_Main

- HOL-Algebra

- HOL-Analysis

For the standard mathematics library, I am aware of [1]. Is this the most

appropriate reference? For HOL-Algebra, I was not able to find any relevant

publications. It seems that [2] is relevant for HOL-Analysis, but I am not

certain if this is the only article and/or the most relevant one, as it

seems to cover only one part of the library. Any help/advice on how to

reference these libraries in the most appropriate manner would be highly

appreciated.

Kind Regards,

Mikhail Chekhov

[1] Hölzl J, Immler F, Huffman B. Type Classes and Filters for Mathematical

Analysis in Isabelle/HOL. In: Blazy S, Paulin-Mohring C, Pichardie D,

editors. Interactive Theorem Proving. Berlin, Heidelberg: Springer Berlin

Heidelberg; 2013. p. 279–94. (Lecture Notes in Computer Science; vol.

7998).

[2] Hölzl J, Heller A. Three Chapters of Measure Theory in Isabelle/HOL.

In: van Eekelen M, Geuvers H, Schmaltz J, Wiedijk F, editors. Interactive

Theorem Proving. Berlin, Heidelberg: Springer Berlin Heidelberg; 2011. p.

135–51. (Lecture Notes in Computer Science; vol. 6898).

Last updated: Dec 08 2021 at 09:20 UTC