X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fpredefined_virtuals.ml;h=a816099a6c901023d9b2c683d09441fdd7e2b9b3;hb=160b7f7385763d872b5f2632696d02fd540c4eae;hp=26a2656e38680b57173338f1ad9081af2affec15;hpb=12dc655b7f5321b33b93a310d53e23e60e090caa;p=helm.git diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 26a2656e3..a816099a6 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1515,13 +1515,13 @@ let predefined_classes = [ ["="; "≝"; "≡"; "≘"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "⊜"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ]; ["→"; "⥲"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; ["⇒"; "⤇"; "➾"; "⇨"; "⬀"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ; - ["^"; "↑"; "⇡"; ] ; + ["^"; "↑"; "⇡"; "↥"; "▵"; ] ; ["⇑"; "⇧"; "⬆"; ] ; ["⇓"; "⇩"; "⬂"; "⬇"; "⬊"; "➷"; ] ; ["⇕"; "⇳"; "⬍"; "↕"; ]; ["↔"; "⇔"; "⬄"; "⬌"; ] ; ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ; - ["_"; "↓"; "↙"; "⇣"; "⇃"; "⇂"; "⎽"; "⎼"; "⎻"; "⎺"; ]; + ["_"; "↓"; "↙"; "⇣"; "⇃"; "⇂"; "⎽"; "⎼"; "⎻"; "⎺"; "▿"; ]; ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ; ["("; "❨"; "❪"; "❲"; "("; ]; [")"; "❩"; "❫"; "❳"; ")"; ]; @@ -1530,7 +1530,7 @@ let predefined_classes = [ ["{"; "❴"; "⦃" ] ; ["}"; "❵"; "⦄" ] ; ["□"; "◽"; "▪"; "◾"; ]; - ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ; + ["◊"; "⬦"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ; [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; "⊃"; "⊐"; ] ; ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; ["∨"; "⩖"; "∪"; "∩"; "⋓"; "⋒" ] ; @@ -1544,7 +1544,7 @@ let predefined_classes = [ ["D"; "Δ"; "𝔻"; "ⅅ"; "𝐃"; "𝚫"; "Ⓓ"; "𝗗"; ] ; ["e"; "ɛ"; "ε"; "ϵ"; "Є"; "ℯ"; "𝕖"; "ⅇ"; "𝐞"; "𝛆"; "𝛜"; "ⓔ"; ] ; ["E"; "ℰ"; "𝔼"; "𝐄"; "Ⓔ"; ] ; - ["f"; "φ"; "ψ"; "ϕ"; "⨍"; "𝕗"; "𝐟"; "𝛟"; "𝛙"; "ⓕ"; ] ; + ["f"; "φ"; "ψ"; "ϕ"; "⨍"; "𝕗"; "𝐟"; "𝛗"; "𝛟"; "𝛙"; "ⓕ"; ] ; ["F"; "Φ"; "Ψ"; "ℱ"; "𝔽"; "𝐅"; "𝚽"; "𝚿"; "Ⓕ"; "𝗙"; ] ; ["g"; "γ"; "ℊ"; "𝕘"; "𝐠"; "𝛄"; "ⓖ"; ] ; ["G"; "Γ"; "𝔾"; "𝐆"; "𝚪"; "Ⓖ"; ] ;