]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/predefined_virtuals.ml
update in ground
[helm.git] / matita / matita / predefined_virtuals.ml
index ead63683a9190738ab7ec0404881924c2eed9cc4..67c3571a48f954de4bd368b4c8b559d542c2ceb7 100644 (file)
@@ -1514,14 +1514,14 @@ let predefined_classes = [
  ["-"; "÷"; "⊢"; "⊩"; "⧟"; "⊟"; ];
  ["="; "≝"; "≡"; "≘"; "≗"; "≐"; "≑"; "≛"; "≚"; "≙"; "⌆"; "⧦"; "⊜"; "≋"; "⩳"; "≅"; "⩬"; "≂"; "≃"; "≈"; ];  
  ["→"; "⥲"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
- ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ;
+ ["â\87\92"; "â¤\87"; "â\9e¾"; "â\87¨"; "â¬\80"; "â\9e¡"; "â¬\88"; "â\9e¤"; "â\9e¸"; "â\87\89"; "⥰"; ] ;
  ["^"; "↑"; "⇡"; ] ;
  ["⇑"; "⇧"; "⬆"; ] ; 
- ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ;
+ ["â\87\93"; "â\87©"; "â¬\82"; "â¬\87"; "â¬\8a"; "â\9e·"; ] ;
  ["⇕"; "⇳"; "⬍"; "↕"; ];
  ["↔"; "⇔"; "⬄"; "⬌"; ] ; 
  ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ;
- ["_"; "↓"; "↙"; "⎽"; "⎼"; "⎻"; "⎺"; ];
+ ["_"; "â\86\93"; "â\86\99"; "â\87£"; "â\87\83"; "â\87\82"; "â\8e½"; "â\8e¼"; "â\8e»"; "â\8eº"; ];
  ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ;
  ["("; "❨"; "❪"; "❲"; "("; ];
  [")"; "❩"; "❫"; "❳"; ")"; ];
@@ -1586,16 +1586,16 @@ let predefined_classes = [
  ["Y"; "ϒ"; "𝕐"; "𝐘"; "𝚼"; "Ⓨ"; ] ;
  ["z"; "ζ"; "𝕫"; "𝐳"; "𝛇"; "ⓩ"; ] ;
  ["Z"; "ℨ"; "ℤ"; "𝐙"; "Ⓩ"; ] ;
- ["0"; "𝟘"; "⓪"; ] ;
- ["1"; "𝟙"; "①"; "⓵"; ] ;
- ["2"; "𝟚"; "②"; "⓶"; ] ;
- ["3"; "𝟛"; "③"; "⓷"; ] ;
- ["4"; "𝟜"; "④"; "⓸"; ] ;
- ["5"; "𝟝"; "⑤"; "⓹"; ] ;
- ["6"; "𝟞"; "⑥"; "⓺"; ] ;
- ["7"; "𝟟"; "⑦"; "⓻"; ] ;
- ["8"; "𝟠"; "⑧"; "⓼"; "∞"; ] ;
- ["9"; "𝟡"; "⑨"; "⓽"; ] ;
+ ["0"; "𝟘"; "⓪"; "𝟎"; ] ;
+ ["1"; "𝟙"; "①"; "⓵"; "𝟏"; ] ;
+ ["2"; "𝟚"; "②"; "⓶"; "𝟐"; ] ;
+ ["3"; "𝟛"; "③"; "⓷"; "𝟑"; ] ;
+ ["4"; "𝟜"; "④"; "⓸"; "𝟒"; ] ;
+ ["5"; "𝟝"; "⑤"; "⓹"; "𝟓"; ] ;
+ ["6"; "𝟞"; "⑥"; "⓺"; "𝟔"; ] ;
+ ["7"; "𝟟"; "⑦"; "⓻"; "𝟕"; ] ;
+ ["8"; "𝟠"; "⑧"; "⓼"; "𝟖"; "∞"; ] ;
+ ["9"; "𝟡"; "⑨"; "⓽"; "𝟗"; ] ;
  ]
 ;;