From 4361c5423d10853505f47e6b2794a54a211a0b44 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 26 Oct 2022 23:43:23 +0200 Subject: [PATCH] update in predefined_virtuals + two arrows added --- matita/matita/predefined_virtuals.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index d59492489..f90ab14bd 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1516,9 +1516,9 @@ let predefined_classes = [ ["+"; "⨭"; "⨮"; "⨁"; "⊕"; "⊞"; ]; ["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ]; ["="; "≝"; "≡"; "≘"; "⊜"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ]; - ["→"; "⥲"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ; + ["→"; "⥲"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "🠢"; "⤳"; ] ; ["⇒"; "⤇"; "➾"; "⇨"; "⬀"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ; - ["^"; "↑"; "⇡"; "↥"; "▵"; ] ; + ["^"; "↑"; "⇡"; "↥"; "🠡"; "▵"; ] ; ["⇑"; "⇧"; "⬆"; ] ; ["⇓"; "⇩"; "⬂"; "⬇"; "⬊"; "➷"; ] ; ["⇕"; "⇳"; "⬍"; "↕"; ]; -- 2.39.2