From fb02b7b3c7caf0b4b5d7d8e41cfef2e637b79026 Mon Sep 17 00:00:00 2001 From: Assia Mahboubi Date: Thu, 30 Nov 2017 16:59:57 +0100 Subject: Minor updates in the readme --- README.md | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/README.md b/README.md index 3dc6c2c..d75aa0b 100644 --- a/README.md +++ b/README.md @@ -2,14 +2,13 @@ # The Mathematical Components repository -The Mathematical Components Library is an extensive body of -mathematics formalized in the Coq/SSReflect language. +The Mathematical Components Library is an extensive and coherent +repository of formalized mathematical theories. It is based on +the [Coq](http://coq.inria.fr) proof assistant, powered with the +[Coq/SSReflect](https://coq.inria.fr/distrib/current/refman/ssreflect.html) +language. -This repository also contains a -[mechanization](https://hal.archives-ouvertes.fr/hal-00816699/) of the -[Odd Order -Theorem](https://en.wikipedia.org/wiki/Feit%E2%80%93Thompson_theorem), -which utilizes the library extensively. +These formal theories cover a wide spectrum of topics, ranging from the formal theory of general purpose data structures like [lists](mathcomp/ssreflect/seq.v), [prime numbers](mathcomp/ssreflect/prime.v) or [finite graphs](mathcomp/ssreflect/fingraph.v), to advanced topics in algebra. The repository includes the socle of formal theories used in a [formal proof](https://www.ams.org/notices/200811/tx081101382p.pdf) of the [Four Colour Theorem](https://en.wikipedia.org/wiki/Four_color_theorem) (Appel - Haken, 1976) and a [mechanization](https://hal.archives-ouvertes.fr/hal-00816699/) of the [Odd Order Theorem](https://en.wikipedia.org/wiki/Feit%E2%80%93Thompson_theorem) (Feit - Thompson, 1963), a landmark result of finite group theory, which utilizes the library extensively. ## Installation @@ -29,17 +28,17 @@ installation instructions in other scenarios. - The [ssreflect mailing list](https://sympa.inria.fr/sympa/info/ssreflect) is the primary venue for help and questions about the library. -- The [MathComp wiki](https://github.com/math-comp/math-comp/wiki) - contains many useful information, including including a list of - [tutorials](https://github.com/math-comp/math-comp/wiki/tutorials) - The [Mathematical Components Book](https://math-comp.github.io/mcb/) provides a comprehensive introduction to the library. +- The [MathComp wiki](https://github.com/math-comp/math-comp/wiki) + contains many useful information, including including a list of + [tutorials](https://github.com/math-comp/math-comp/wiki/tutorials). - Experienced users hang around at [StackOverflow](https://stackoverflow.com/questions/tagged/ssreflect) listening to the `ssreflect` and `coq` tags. ## Publications and Tools using MathComp -[Papers](https://github.com/math-comp/math-comp/wiki/Publications) -using the Mathematical Components library can be found at the -[wiki](https://github.com/math-comp/math-comp/wiki) +A collection of [papers](https://github.com/math-comp/math-comp/wiki/Publications) +using the Mathematical Components library can be found on the +[wiki](https://github.com/math-comp/math-comp/wiki). -- cgit v1.2.3