X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fpredefined_virtuals.ml;h=45f3829dd789b67f361b59bea3d925281d1a85f0;hb=refs%2Fheads%2Fmaster;hp=92cb18cfac13d75ee81c0660b959b9ac473f1786;hpb=2c68dcfee2c3fe819c8f92a9609620a85909ce8a;p=helm.git diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 92cb18cfa..45f3829dd 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1497,12 +1497,14 @@ let predefined_virtuals = [ let load_predefined_virtuals () = List.iter - (fun a,b,c -> + (fun (a,b,c) -> Virtuals.add_virtual a (Glib.Utf8.first_char b) c) predefined_virtuals ;; let predefined_classes = [ + ["@"; "@"; ]; + ["*"; "∗"; ]; ["/"; "⧸"; ]; ["&"; "⅋"; ]; ["|"; "❘"; "∥"; ]; @@ -1510,19 +1512,19 @@ let predefined_classes = [ ["?"; "¿"; "⸮"; ]; [":"; "⁝"; ]; ["."; "•"; "◦"; ]; - ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ]; + ["#"; "♯"; "⋕"; "⧣"; "⧤"; "♮"; "⌘"; ]; ["+"; "⨭"; "⨮"; "⨁"; "⊕"; "⊞"; ]; ["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ]; ["="; "≝"; "≡"; "≘"; "⊜"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ]; - ["→"; "⥲"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; + ["→"; "⥲"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "🠢"; "⤳"; ] ; ["⇒"; "⤇"; "➾"; "⇨"; "⬀"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ; - ["^"; "↑"; "⇡"; "↥"; "▵"; ] ; + ["^"; "↑"; "⇡"; "↥"; "🠡"; "▵"; ] ; ["⇑"; "⇧"; "⬆"; ] ; ["⇓"; "⇩"; "⬂"; "⬇"; "⬊"; "➷"; ] ; ["⇕"; "⇳"; "⬍"; "↕"; ]; ["↔"; "⇔"; "⬄"; "⬌"; ] ; ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ; - ["_"; "↓"; "↙"; "⇣"; "⇃"; "⇂"; "⎽"; "⎼"; "⎻"; "⎺"; "▿"; ]; + ["_"; "↓"; "↙"; "⇣"; "⇃"; "⇂"; "↳"; "⎽"; "⎼"; "⎻"; "⎺"; "▿"; ]; ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ; ["("; "❨"; "❪"; "❲"; "("; ]; [")"; "❩"; "❫"; "❳"; ")"; ]; @@ -1531,7 +1533,7 @@ let predefined_classes = [ ["{"; "❴"; "⦃" ] ; ["}"; "❵"; "⦄" ] ; ["□"; "◽"; "▪"; "◾"; ]; - ["◊"; "⬦"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ; + ["◊"; "⬦"; "♢"; "◆"; "⧫"; "♦"; "⟐"; "⟠"; ] ; [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; "⊃"; "⊐"; ] ; ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; ["∨"; "⩖"; "∪"; "∩"; "⋓"; "⋒" ] ; @@ -1570,7 +1572,7 @@ let predefined_classes = [ ["q"; "𝕢"; "𝐪"; "ⓠ"; ] ; ["Q"; "ℚ"; "𝐐"; "Ⓠ"; ] ; ["r"; "ρ"; "ϱ"; "𝕣"; "𝐫"; "𝛒"; "𝛠"; "ⓡ"; ] ; - ["R"; "ℛ"; "ℜ"; "ℝ"; "𝐑"; "Ⓡ"; ] ; + ["R"; "ℛ"; "ℜ"; "ℝ"; "𝐑"; "Ⓡ"; "ᴿ"; ] ; ["s"; "σ"; "ς"; "𝕤"; "𝐬"; "𝛔"; "ⓢ"; ] ; ["S"; "Σ"; "𝕊"; "𝐒"; "𝚺"; "Ⓢ"; "𝗦"; ] ; ["t"; "τ"; "𝕥"; "𝐭"; "𝛕"; "ⓣ"; ] ;