X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fpredefined_virtuals.ml;h=f90ab14bdbe39c9352c1167faa4b7ea1c5a47326;hb=4361c5423d10853505f47e6b2794a54a211a0b44;hp=2ec69e63f23b7b0e55cbc6ea927b3c9e871e8d44;hpb=13584a37bbcde10e03c8a488f5b93e1e042da0a6;p=helm.git diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 2ec69e63f..f90ab14bd 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1503,6 +1503,8 @@ let load_predefined_virtuals () = ;; let predefined_classes = [ + ["@"; "@"; ]; + ["*"; "∗"; ]; ["/"; "⧸"; ]; ["&"; "⅋"; ]; ["|"; "❘"; "∥"; ]; @@ -1510,19 +1512,19 @@ let predefined_classes = [ ["?"; "¿"; "⸮"; ]; [":"; "⁝"; ]; ["."; "•"; "◦"; ]; - ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ]; + ["#"; "♯"; "⋕"; "⧣"; "⧤"; "♮"; "⌘"; ]; ["+"; "⨭"; "⨮"; "⨁"; "⊕"; "⊞"; ]; ["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ]; ["="; "≝"; "≡"; "≘"; "⊜"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ]; - ["→"; "⥲"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; + ["→"; "⥲"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "🠢"; "⤳"; ] ; ["⇒"; "⤇"; "➾"; "⇨"; "⬀"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ; - ["^"; "↑"; "⇡"; "↥"; "▵"; ] ; + ["^"; "↑"; "⇡"; "↥"; "🠡"; "▵"; ] ; ["⇑"; "⇧"; "⬆"; ] ; ["⇓"; "⇩"; "⬂"; "⬇"; "⬊"; "➷"; ] ; ["⇕"; "⇳"; "⬍"; "↕"; ]; ["↔"; "⇔"; "⬄"; "⬌"; ] ; ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ; - ["_"; "↓"; "↙"; "⇣"; "⇃"; "⇂"; "⎽"; "⎼"; "⎻"; "⎺"; "▿"; ]; + ["_"; "↓"; "↙"; "⇣"; "⇃"; "⇂"; "↳"; "⎽"; "⎼"; "⎻"; "⎺"; "▿"; ]; ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ; ["("; "❨"; "❪"; "❲"; "("; ]; [")"; "❩"; "❫"; "❳"; ")"; ]; @@ -1531,13 +1533,13 @@ let predefined_classes = [ ["{"; "❴"; "⦃" ] ; ["}"; "❵"; "⦄" ] ; ["□"; "◽"; "▪"; "◾"; ]; - ["◊"; "⬦"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ; + ["◊"; "⬦"; "♢"; "◆"; "⧫"; "♦"; "⟐"; "⟠"; ] ; [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; "⊃"; "⊐"; ] ; ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; ["∨"; "⩖"; "∪"; "∩"; "⋓"; "⋒" ] ; ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ; ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; "𝗔"; ] ; - ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ; + ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; "♭"; ] ; ["B"; "ℶ"; "ℬ"; "𝔹"; "𝐁"; "Ⓑ"; ] ; ["c"; "𝕔"; "𝐜"; "ⓒ"; ] ; ["C"; "ℭ"; "∁"; "𝐂"; "ℂ"; "Ⓒ"; ] ; @@ -1570,7 +1572,7 @@ let predefined_classes = [ ["q"; "𝕢"; "𝐪"; "ⓠ"; ] ; ["Q"; "ℚ"; "𝐐"; "Ⓠ"; ] ; ["r"; "ρ"; "ϱ"; "𝕣"; "𝐫"; "𝛒"; "𝛠"; "ⓡ"; ] ; - ["R"; "ℛ"; "ℜ"; "ℝ"; "𝐑"; "Ⓡ"; ] ; + ["R"; "ℛ"; "ℜ"; "ℝ"; "𝐑"; "Ⓡ"; "ᴿ"; ] ; ["s"; "σ"; "ς"; "𝕤"; "𝐬"; "𝛔"; "ⓢ"; ] ; ["S"; "Σ"; "𝕊"; "𝐒"; "𝚺"; "Ⓢ"; "𝗦"; ] ; ["t"; "τ"; "𝕥"; "𝐭"; "𝛕"; "ⓣ"; ] ;