1 |
|
2 |
|
3 |
|
4 |
|
5 |
|
6 |
|
7 |
|
8 |
|
9 | function mizar(hljs) {
|
10 | return {
|
11 | name: 'Mizar',
|
12 | keywords:
|
13 | 'environ vocabularies notations constructors definitions ' +
|
14 | 'registrations theorems schemes requirements begin end definition ' +
|
15 | 'registration cluster existence pred func defpred deffunc theorem ' +
|
16 | 'proof let take assume then thus hence ex for st holds consider ' +
|
17 | 'reconsider such that and in provided of as from be being by means ' +
|
18 | 'equals implies iff redefine define now not or attr is mode ' +
|
19 | 'suppose per cases set thesis contradiction scheme reserve struct ' +
|
20 | 'correctness compatibility coherence symmetry assymetry ' +
|
21 | 'reflexivity irreflexivity connectedness uniqueness commutativity ' +
|
22 | 'idempotence involutiveness projectivity',
|
23 | contains: [
|
24 | hljs.COMMENT('::', '$')
|
25 | ]
|
26 | };
|
27 | }
|
28 |
|
29 | export { mizar as default };
|