X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fpredefined_virtuals.ml;h=6b259a253d47a7c091117387a81115dcff9c44c1;hb=756e320c149ae141dffbf5d75202c8e46c4a49b9;hp=d4f38b0baead585e99570b7caff1e34cb80ce0d3;hpb=11792b819aba3f464e63cb8f7834cac1652e372a;p=helm.git diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index d4f38b0ba..6b259a253 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1505,22 +1505,22 @@ let load_predefined_virtuals () = let predefined_classes = [ ["&"; "⅋"; ]; ["|"; "∥"; ]; - ["!"; "¡"; "⫯"; "⫰"; ]; + ["!"; "¡"; "⫯"; "⫰"; "⟟"; "⫱"; ]; ["?"; "¿"; "⸮"; ]; [":"; "⁝"; ]; ["."; "•"; "◦"; ]; ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ]; ["+"; "⊞"; ]; ["-"; "÷"; "⊢"; "⊩"; "⊟"; ]; - ["="; "≝"; "≡"; "⩬"; "≂"; "≃"; "≈"; "≅"; "≐"; "≑"; "≚"; "≙"; "⌆"; "⊜"; ]; + ["="; "≝"; "≡"; "⩬"; "≂"; "≃"; "≈"; "≅"; "≗"; "≐"; "≑"; "≚"; "≙"; "⌆"; "⊜"; ]; ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; - ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "➤"; "➸"; "⇉"; "⥰"; ] ; + ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ; ["^"; "↑"; ] ; ["⇑"; "⇧"; "⬆"; ] ; ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ; ["⇕"; "⇳"; "⬍"; ]; ["↔"; "⇔"; "⬄"; "⬌"; ] ; - ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ]; + ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ; ["_"; "↓"; "↙"; "⎽"; "⎼"; "⎻"; "⎺"; ]; ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ; ["("; "❨"; "❪"; "❲"; "("; ]; @@ -1533,7 +1533,7 @@ let predefined_classes = [ ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ; [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; "⊃"; "⊐"; ] ; ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; - ["∨"; "⩖"; "⋓"; ] ; + ["∨"; "⩖"; "∪"; "∩"; "⋓"; "⋒" ] ; ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ; ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ; ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ;