X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fpredefined_virtuals.ml;h=8fd858f545dba17a7256953e97ddf911f5be23f6;hb=fbb1435e16f0c737f3941fae83140a7d6454997e;hp=4d86409b70147f19adb3aa42e3cc93c25c7952d6;hpb=1f1ea7bb9e6c34626bcabd4c0142fcde98bcbbe5;p=helm.git diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 4d86409b7..8fd858f54 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1503,18 +1503,21 @@ let load_predefined_virtuals () = ;; let predefined_classes = [ + ["!"; "¡"; "⫯"; "⫰"; ]; + ["?"; "¿"; "⸮"; ]; [":"; "⁝"; ]; ["."; "•"; "◦"; ]; - ["#"; "⌘"; ]; + ["#"; "♯"; "⋕"; "⌘"; ]; ["-"; "÷"; "⊢"; "⊩"; ]; - ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ]; - ["→"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; - ["⇒"; "➾"; "⇨"; "➡"; "➸"; "⇉"; "⥤"; "⥰"; ] ; + ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; "≚"; "≙"; "⌆"; ]; + ["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; + ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "➤"; "➸"; "⇉"; "⥰"; ] ; + ["^"; "↑"; ] ; ["⇑"; "⇧"; "⬆"; ] ; ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ; ["↔"; "⇔"; "⬄"; "⬌"; ] ; - ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; ]; - ["_" ; "⎽"; "⎼"; "⎻"; "⎺"; ]; + ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊑"; ]; + ["_"; "↓"; "↙"; "⎽"; "⎼"; "⎻"; "⎺"; ]; ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ; ["("; "❨"; "❪"; "❲"; "("; ]; [")"; "❩"; "❫"; "❳"; ")"; ]; @@ -1524,8 +1527,8 @@ let predefined_classes = [ ["}"; "❵"; "⦄" ] ; ["□"; "◽"; "▪"; "◾"; ]; ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ; - [">"; "⭃"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ; - ["≥"; "≽"; "⥸"; ]; + [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ; + ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ; ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ; ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ; @@ -1586,7 +1589,7 @@ let predefined_classes = [ ["5"; "𝟝"; "⑤"; "⓹"; ] ; ["6"; "𝟞"; "⑥"; "⓺"; ] ; ["7"; "𝟟"; "⑦"; "⓻"; ] ; - ["8"; "𝟠"; "⑧"; "⓼"; ] ; + ["8"; "𝟠"; "⑧"; "⓼"; "∞"; ] ; ["9"; "𝟡"; "⑨"; "⓽"; ] ; ] ;;