File tree 2 files changed +14
-6
lines changed
2 files changed +14
-6
lines changed Original file line number Diff line number Diff line change 4
4
< html xmlns ="http://www.w3.org/1999/xhtml " lang ="en " xml:lang ="en ">
5
5
< head >
6
6
< title > Mathematical Components</ title >
7
- <!-- 2019-07-03 mer. 17:29 -->
7
+ <!-- 2019-07-03 mer. 17:31 -->
8
8
< meta http-equiv ="Content-Type " content ="text/html;charset=utf-8 " />
9
9
< meta name ="generator " content ="Org-mode " />
10
10
< meta name ="author " content ="assia " />
@@ -162,17 +162,22 @@ <h2 id="sec-1">About</h2>
162
162
developed using the < a href ="http://coq.inria.fr "> Coq</ a > proof assistant. This project finds its roots
163
163
in the formal proof of the Four Color Theorem. It has been used for
164
164
large scale formalization projects, including a formal proof of the
165
- Odd Order (Feit-Thompson) Theorem.
165
+ Odd Order
166
+ (Feit-Thompson) Theorem.
166
167
</ p >
167
168
168
169
< p >
169
- The library is written using the Ssreflect proof language, now part of
170
+ The libraries are written using the Ssreflect proof language, now part of
170
171
the standard distribution of the Coq proof assistant.
171
172
</ p >
173
+
174
+ < p >
175
+ This is an open source project, licensed under the CeCILL-B free
176
+ software license agreement.
177
+ </ p >
172
178
</ div >
173
179
</ div >
174
180
175
-
176
181
< div id ="outline-container-sec-2 " class ="outline-2 ">
177
182
< h2 id ="sec-2 "> Get the library</ h2 >
178
183
< div class ="outline-text-2 " id ="text-2 ">
Original file line number Diff line number Diff line change @@ -22,11 +22,14 @@ Mathematical Components are libraries of formalized mathematics
22
22
developed using the [[http://coq.inria.fr][Coq]] proof assistant. This project finds its roots
23
23
in the formal proof of the Four Color Theorem. It has been used for
24
24
large scale formalization projects, including a formal proof of the
25
- Odd Order (Feit-Thompson) Theorem.
25
+ Odd Order
26
+ (Feit-Thompson) Theorem.
26
27
27
- The library is written using the Ssreflect proof language, now part of
28
+ The libraries are written using the Ssreflect proof language, now part of
28
29
the standard distribution of the Coq proof assistant.
29
30
31
+ This is an open source project, licensed under the CeCILL-B free
32
+ software license agreement.
30
33
31
34
* Get the library
32
35
You can’t perform that action at this time.
0 commit comments