isarmathlib-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Isarmathlib-devel] IsarMathLib 1.8.0 released


From: Slawomir Kolodynski
Subject: [Isarmathlib-devel] IsarMathLib 1.8.0 released
Date: Mon, 4 Mar 2013 10:48:29 -0800 (PST)

Following the Isabelle2013 release I have released IsarMathLib 1.8.0. The new stuff comprises 5 new theory files about general topology (convergence of nets and filters and related continuity properties of functions, generalizations of compactness and connectedness, heredity and spectra of topological properties), contributed by Daniel de la Concepción Sáez. I finished the proof of continuity of sum of a list of elements of a topological group. The ROOT.ML file was replaced by the ROOT file with new syntax defining IsarMathLib as an Isabelle session. Since IsaMakefile is not there anymore, do "isabelle build -D ./IsarMathLib" from the directory where it used to be to verify the theories and create the proof document and outline.

slawekk

http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)

reply via email to

[Prev in Thread] Current Thread [Next in Thread]