[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Extended ASCII
We plan to elimante Extended ASCII from Mizar. It forces
us to exchange some symbols in current MML. The job can
be divided into three steps:
1. Exchange of attribute and mode symbols,
2. Exchange of predicate symbols,
3. Exchange of functor symbols.
We present suggestions concerning the first step.
What is your opinion?
In the text below Extended ASCII characters are encoded according to
http://mizar.org/JFM/ASCII/ExtAscii.html ('#'decimal_number)
A T T R I B U T E S
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
-1-
:: Atlas of Midpoint Algebra
:: by Micha{\l} Muzalewski
:: MIDSP_2: def 5
attr Group_with_the_operator_#171-like
http://mizar.org/JFM/Vol3/midsp_2.abs.html#V1
*** Suggestion: midpoint_operator
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
-2-
:: Quantales
:: by Grzegorz Bancerek
:: QUANTAL1: def 7
attr #224-additive
http://mizar.org/JFM/Vol6/quantal1.abs.html#V9
*** Suggestion: times-additive
:: QUANTAL1: def 8
attr #224-continuous
http://mizar.org/JFM/Vol6/quantal1.abs.html#V10
*** Suggestion: times-continuous
:: QUANTAL1: def 14
attr #224-monotone
http://mizar.org/JFM/Vol6/quantal1.abs.html#V16
*** Suggestion: times-monotone
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
-3-
:: The $\sigma$-additive Measure Theory
:: by J\'ozef Bia{\l}as
:: MEASURE1: def 9
attr #229_Field_Subset-like
http://mizar.org/JFM/Vol2/measure1.abs.html#V4
*** Suggestion: sigma_Field_Subset-like
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
-4-
:: Algebra of Morphisms
:: by Grzegorz Bancerek
:: CATALG_1: def 9
attr #235-concrete
http://mizar.org/JFM/Vol9/catalg_1.abs.html#V5
*** Suggestion: delta-concrete
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
-5-
:: The Limit of a Real Function at Infinity. Halflines.
:: Real Sequence Divergent to Infinity
:: by Jaros{\l}aw Kotowicz
:: LIMFUNC1: def 4
attr divergent_to_+#236
http://mizar.org/JFM/Vol2/limfunc1.abs.html#V1
*** Suggestion: divergent_to+infty
:: LIMFUNC1: def 5
attr divergent_to_-#236
http://mizar.org/JFM/Vol2/limfunc1.abs.html#V2
*** Suggestion: divergent_to-infty
:: LIMFUNC1: def 6
attr convergent_in_+#236
http://mizar.org/JFM/Vol2/limfunc1.abs.html#V3
*** Suggestion: convergent_in+infty
:: LIMFUNC1: def 7
attr divergent_in_+#236_to_+#236
http://mizar.org/JFM/Vol2/limfunc1.abs.html#V4
*** Suggestion: divergent_in+infty_to+infty
:: LIMFUNC1: def 8
attr divergent_in_+#236_to_-#236
http://mizar.org/JFM/Vol2/limfunc1.abs.html#V5
*** Suggestion: divergent_in+infty_to-infty
:: LIMFUNC1: def 9
attr convergent_in_-#236
http://mizar.org/JFM/Vol2/limfunc1.abs.html#V6
*** Suggestion: convergent_in-infty
:: LIMFUNC1: def 10
attr divergent_in_-#236_to_+#236
http://mizar.org/JFM/Vol2/limfunc1.abs.html#V7
*** Suggestion: divergent_in-infty_to+infty
:: LIMFUNC1: def 11
attr divergent_in_-#236_to_-#236
http://mizar.org/JFM/Vol2/limfunc1.abs.html#V8
*** Suggestion: divergent_in-infty_to-infty
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
-6-
:: The Ordinal Numbers. Transfinite Induction and Defining by
:: Transfinite Induction
:: by Grzegorz Bancerek
:: ORDINAL1: def 2
attr #238-transitive
http://mizar.org/JFM/Vol1/ordinal1.abs.html#V1
*** Suggestion: epsilon-transitive
:: ORDINAL1: def 3
attr #238-connected
http://mizar.org/JFM/Vol1/ordinal1.abs.html#V2
*** Suggestion: epsilon-connected
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
-7-
:: Continuous, Stable, and Linear Maps of Coherence Spaces
:: by Grzegorz Bancerek
:: COHSP_1: def 4
attr U-directed
http://mizar.org/JFM/Vol7/cohsp_1.abs.html#V1
*** Suggestion: c=directed
:: COHSP_1: def 5
attr #239-directed
http://mizar.org/JFM/Vol7/cohsp_1.abs.html#V2
*** Suggestion c=filtered
:: COHSP_1: def 6
attr #239-closed
http://mizar.org/JFM/Vol7/cohsp_1.abs.html#V3
*** Suggestion: multiplicative
:: COHSP_1: def 13
attr #239-distributive
http://mizar.org/JFM/Vol7/cohsp_1.abs.html#V8
*** Suggestion: cap-distributive
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
M O D E S
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
-1-
:: Atlas of Midpoint Algebra
:: by Micha{\l} Muzalewski
:: MIDSP_2
mode Group_with_the_operator_#171
http://mizar.org/JFM/Vol3/midsp_2.abs.html#X2
*** Suggestion: - removed
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
-2-
:: On the Lattice of Subspaces of Vector Space
:: by Andrzej Iwaniuk
:: VECTSP_8: def 8
mode #218#191-Homomorphism
http://mizar.org/JFM/Vol7/vectsp_8.abs.html#M3
*** Suggestion: Semilattice-Homomorphism
:: VECTSP_8: def 9
mode #192#217-Homomorphism
http://mizar.org/JFM/Vol7/vectsp_8.abs.html#M4
*** Suggestion: sup-Semilattice-Homomorphism
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
-3-
:: On the Decomposition of the Continuity
:: by Marian Przemski
:: DECOMP_1: def 1
mode #224-set
http://mizar.org/JFM/Vol6/decomp_1.abs.html#M1
*** Suggestion: alpha-set
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
-4-
:: The $\sigma$-additive Measure Theory
:: by J\'ozef Bia{\l}as
:: MEASURE1
mode #229_Field_Subset of X
http://mizar.org/JFM/Vol2/measure1.abs.html#X6
*** Suggestion: sigma_Field_Subset
:: MEASURE1: def 11
mode #229_Measure of S
http://mizar.org/JFM/Vol2/measure1.abs.html#M5
*** Suggestion: sigma_Measure
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
-5-
:: Special Polygons
:: by Czes\law Byli\'nski and Yatsuka Nakamura
:: SPPOL_2
mode S-Sequence_in_R#253
http://mizar.org/JFM/Vol7/sppol_2.abs.html#X1
*** Suggestion: S-Sequence_in_R2
:: SPPOL_2
mode Special_polygon_in_R#253
http://mizar.org/JFM/Vol7/sppol_2.abs.html#X2
*** Suggestion: Special_polygon_in_R2
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Robert Milewski
Institute of Mathematics
University in Bialystok
milewski@mizar.org