update in predefined_virtuals

[helm.git] / matita / matita / predefined_virtuals.ml

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 6b259a253d47a7c091117387a81115dcff9c44c1..f90ab14bdbe39c9352c1167faa4b7ea1c5a47326 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1503,49 +1503,52 @@ let load_predefined_virtuals () =
 ;;
 
 let predefined_classes = [
+ ["@"; "＠"; ];
+ ["*"; "∗"; ];
+ ["/"; "⧸"; ];
  ["&"; "⅋"; ];
- ["|"; "∥"; ];
+ ["|"; "â\9d\98"; "â\88¥"; ];
  ["!"; "¡"; "⫯"; "⫰"; "⟟"; "⫱"; ];
  ["?"; "¿"; "⸮"; ];
  [":"; "⁝"; ];
  ["."; "•"; "◦"; ];
- ["#"; "♯"; "⋕"; "⧣"; "⧤"; "⌘"; ];
- ["+"; "⊞"; ];
- ["-"; "÷"; "⊢"; "⊩"; "⊟"; ];
- ["="; "â\89\9d"; "â\89¡"; "⩬"; "â\89\82"; "â\89\83"; "â\89\88"; "â\89\85"; "â\89\97"; "â\89\90"; "â\89\91"; "â\89\9a"; "â\89\99"; "â\8c\86"; "â\8a\9c"; ];  
- ["â\86\92"; "â\86¦"; "â\87\9d"; "â¤\9e"; "â\87¾"; "â¤\8d"; "â¤\8f"; "⤳"; ] ;
- ["⇒"; "⤇"; "➾"; "⇨"; "➡"; "⬈"; "➤"; "➸"; "⇉"; "⥰"; ] ;
- ["^"; "↑"; ] ;
+ ["#"; "â\99¯"; "â\8b\95"; "⧣"; "⧤"; "â\99®"; "â\8c\98"; ];
+ ["+"; "⨭"; "⨮"; "â¨\81"; "â\8a\95"; "â\8a\9e"; ];
+ ["-"; "÷"; "â\8a¢"; "â\8a©"; "â§\9f"; "â\8a\9f"; ];
+ ["="; "â\89\9d"; "â\89¡"; "â\89\98"; "â\8a\9c"; "â\89\97"; "â\89\90"; "â\89\91"; "â\89\9b"; "â\89\9a"; "â\89\99"; "â\8c\86"; "⧦"; "â\89\8b"; "⩳"; "â\89\85"; "⩬"; "â\89\82"; "â\89\83"; "â\89\88"; ];
+ ["â\86\92"; "⥲"; "â\86¦"; "â\87\9d"; "â¤\9e"; "â\87¾"; "â¤\8d"; "â¤\8f"; "ð\9f ¢"; "⤳"; ] ;
+ ["â\87\92"; "â¤\87"; "â\9e¾"; "â\87¨"; "â¬\80"; "â\9e¡"; "â¬\88"; "â\9e¤"; "â\9e¸"; "â\87\89"; "⥰"; ] ;
+ ["^"; "↑"; "⇡"; "↥"; "🠡"; "▵"; ] ;
  ["⇑"; "⇧"; "⬆"; ] ; 
- ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ;
- ["⇕"; "⇳"; "⬍"; ];
+ ["â\87\93"; "â\87©"; "â¬\82"; "â¬\87"; "â¬\8a"; "â\9e·"; ] ;
+ ["⇕"; "⇳"; "⬍"; "↕"; ];
  ["↔"; "⇔"; "⬄"; "⬌"; ] ; 
  ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ;
- ["_"; "â\86\93"; "â\86\99"; "â\8e½"; "â\8e¼"; "â\8e»"; "â\8eº"; ];
+ ["_"; "â\86\93"; "â\86\99"; "â\87£"; "â\87\83"; "â\87\82"; "â\86³"; "â\8e½"; "â\8e¼"; "â\8e»"; "â\8eº"; "â\96¿"; ];
  ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ;
  ["("; "❨"; "❪"; "❲"; "（"; ];
  [")"; "❩"; "❫"; "❳"; "）"; ];
- ["["; "⦋"; "〚"; ] ;
- ["]"; "⦌"; "〛"; ] ;
+ ["["; "⦋"; "⟦"; ] ;
+ ["]"; "⦌"; "⟧"; ] ;
  ["{"; "❴"; "⦃" ] ;
  ["}"; "❵"; "⦄" ] ;
  ["□"; "◽"; "▪"; "◾"; ];
- ["â\97\8a"; "â\99¢"; "⧫"; "♦"; "⟐"; "⟠"; ] ;
+ ["â\97\8a"; "⬦"; "â\99¢"; "â\97\86"; "⧫"; "♦"; "⟐"; "⟠"; ] ;
  [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; "⊃"; "⊐"; ] ;
  ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; 
  ["∨"; "⩖"; "∪"; "∩"; "⋓"; "⋒" ] ;
  ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ;
- ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ;
- ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ;
+ ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; "𝗔"; ] ;
+ ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; "♭"; ] ;
  ["B"; "ℶ"; "ℬ"; "𝔹"; "𝐁"; "Ⓑ"; ] ;
  ["c"; "𝕔"; "𝐜"; "ⓒ"; ] ;
- ["C"; "ℭ"; "∁"; "𝐂"; "Ⓒ"; ] ;
- ["d"; "δ"; "∂"; "𝕕"; "ⅆ"; "𝐝"; "𝛅"; "ⓓ"; ] ;
- ["D"; "Δ"; "𝔻"; "ⅅ"; "𝐃"; "𝚫"; "Ⓓ"; ] ;
+ ["C"; "â\84­"; "â\88\81"; "ð\9d\90\82"; "â\84\82"; "â\92¸"; ] ;
+ ["d"; "δ"; "∂"; "𝕕"; "ⅆ"; "𝐝"; "𝛅"; "ⓓ"; "𝗱"; ] ;
+ ["D"; "Δ"; "𝔻"; "ⅅ"; "𝐃"; "𝚫"; "Ⓓ"; "𝗗"; ] ;
  ["e"; "ɛ"; "ε"; "ϵ"; "Є"; "ℯ"; "𝕖"; "ⅇ"; "𝐞"; "𝛆"; "𝛜"; "ⓔ"; ] ;
  ["E"; "ℰ"; "𝔼"; "𝐄"; "Ⓔ"; ] ;
- ["f"; "φ"; "ψ"; "ϕ"; "⨍"; "𝕗"; "𝐟"; "𝛟"; "𝛙"; "ⓕ"; ] ;
- ["F"; "Φ"; "Ψ"; "ℱ"; "𝔽"; "𝐅"; "𝚽"; "𝚿"; "Ⓕ"; ] ;
+ ["f"; "Ï\86"; "Ï\88"; "Ï\95"; "â¨\8d"; "ð\9d\95\97"; "ð\9d\90\9f"; "ð\9d\9b\97"; "ð\9d\9b\9f"; "ð\9d\9b\99"; "â\93\95"; ] ;
+ ["F"; "Φ"; "Ψ"; "ℱ"; "𝔽"; "𝐅"; "𝚽"; "𝚿"; "Ⓕ"; "𝗙"; ] ;
  ["g"; "γ"; "ℊ"; "𝕘"; "𝐠"; "𝛄"; "ⓖ"; ] ;
  ["G"; "Γ"; "𝔾"; "𝐆"; "𝚪"; "Ⓖ"; ] ;
  ["h"; "η"; "ℌ"; "ℎ"; "𝕙"; "𝐡"; "ⓗ"; ] ;
@@ -1557,45 +1560,45 @@ let predefined_classes = [
  ["k"; "κ"; "𝕜"; "𝐤"; "𝛋"; "ⓚ"; ] ;
  ["K"; "𝕂"; "𝐊"; "Ⓚ"; ] ;
  ["l"; "λ"; "𝕝"; "𝐥"; "𝛌"; "ⓛ"; ] ;
- ["L"; "Λ"; "𝕃"; "𝐋"; "𝚲"; "Ⓛ"; ] ;
- ["m"; "μ"; "𝕞"; "𝐦"; "𝛍"; "ⓜ"; ] ;
+ ["L"; "Λ"; "𝕃"; "𝐋"; "𝚲"; "Ⓛ"; "𝗟"; ] ;
+ ["m"; "μ"; "𝕞"; "𝐦"; "𝛍"; "ⓜ"; "𝗺"; "ɱ"; ] ;
  ["M"; "ℳ"; "𝕄"; "𝐌"; "Ⓜ"; ] ;
  ["n"; "𝕟"; "𝐧"; "𝛈"; "ⓝ"; ] ;
  ["N"; "ℕ"; "№"; "𝐍"; "Ⓝ"; ] ;
- ["o"; "θ"; "ϑ"; "𝕠"; "∘";  "⊚"; "ø"; "○"; "𝐨"; "𝛉"; "ⓞ"; ] ;
+ ["o"; "θ"; "ϑ"; "𝕠"; "∘";  "⊚"; "ø"; "○"; "●"; "◖"; "◗"; "𝐨"; "𝛉"; "ⓞ"; ] ;
  ["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹"; "Ⓞ"; ] ;
  ["p"; "π"; "𝕡"; "𝐩"; "𝛑"; "ⓟ"; ] ;
- ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; ] ;
+ ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; "𝒫"; "Ꝕ"; ] ;
  ["q"; "𝕢"; "𝐪"; "ⓠ"; ] ;
  ["Q"; "ℚ"; "𝐐"; "Ⓠ"; ] ;
  ["r"; "ρ"; "ϱ"; "𝕣"; "𝐫"; "𝛒"; "𝛠"; "ⓡ"; ] ;
- ["R"; "ℛ"; "ℜ"; "ℝ"; "𝐑"; "Ⓡ"; ] ;
+ ["R"; "ℛ"; "ℜ"; "ℝ"; "𝐑"; "Ⓡ"; "ᴿ"; ] ;
  ["s"; "σ"; "ς"; "𝕤"; "𝐬"; "𝛔"; "ⓢ"; ] ;
- ["S"; "Σ"; "𝕊"; "𝐒"; "𝚺"; "Ⓢ"; ] ;
+ ["S"; "Σ"; "𝕊"; "𝐒"; "𝚺"; "Ⓢ"; "𝗦"; ] ;
  ["t"; "τ"; "𝕥"; "𝐭"; "𝛕"; "ⓣ"; ] ;
- ["T"; "𝕋"; "𝐓"; "Ⓣ"; "⊥"; ] ;
+ ["T"; "𝕋"; "𝐓"; "Ⓣ"; "Ƭ"; "⊥"; ] ;
  ["u"; "𝕦"; "𝐮"; "ⓤ"; ] ;
  ["U"; "𝕌"; "𝐔"; "Ⓤ"; ] ;
  ["v"; "ν"; "𝕧"; "𝐯"; "𝛖"; "𝛎"; "ⓥ"; "▼"; ] ;
  ["V"; "𝕍"; "𝐕"; "Ⓥ"; ] ;
  ["w"; "ω"; "𝕨"; "𝐰"; "𝛚"; "ⓦ"; ] ;
  ["W"; "Ω"; "𝕎"; "𝐖"; "𝛀"; "Ⓦ"; ] ;
- ["x"; "ξ"; "χ"; "ϰ"; "𝕩"; "𝐱"; "𝛏"; "𝛘"; "𝛞"; "ⓧ"; ] ;
- ["X"; "Ξ"; "𝕏";"𝐗"; "𝚵"; "Ⓧ"; "⦻"; ] ;
+ ["x"; "ξ"; "χ"; "ϰ"; "𝕩"; "𝐱"; "𝛏"; "𝛘"; "𝛞"; "ⓧ"; "⨴"; "⨵"; ] ;
+ ["X"; "Ξ"; "𝕏";"𝐗"; "𝚵"; "Ⓧ"; "⦻"; "⪤" ] ;
  ["y"; "υ"; "𝕪"; "𝐲"; "ⓨ"; ] ;
  ["Y"; "ϒ"; "𝕐"; "𝐘"; "𝚼"; "Ⓨ"; ] ;
  ["z"; "ζ"; "𝕫"; "𝐳"; "𝛇"; "ⓩ"; ] ;
  ["Z"; "ℨ"; "ℤ"; "𝐙"; "Ⓩ"; ] ;
- ["0"; "𝟘"; "⓪"; ] ;
- ["1"; "𝟙"; "①"; "⓵"; ] ;
- ["2"; "𝟚"; "②"; "⓶"; ] ;
- ["3"; "𝟛"; "③"; "⓷"; ] ;
- ["4"; "𝟜"; "④"; "⓸"; ] ;
- ["5"; "𝟝"; "⑤"; "⓹"; ] ;
- ["6"; "𝟞"; "⑥"; "⓺"; ] ;
- ["7"; "𝟟"; "⑦"; "⓻"; ] ;
- ["8"; "𝟠"; "⑧"; "⓼"; "∞"; ] ;
- ["9"; "𝟡"; "⑨"; "⓽"; ] ;
+ ["0"; "𝟘"; "⓪"; "𝟎"; ] ;
+ ["1"; "𝟙"; "①"; "⓵"; "𝟏"; ] ;
+ ["2"; "𝟚"; "②"; "⓶"; "𝟐"; ] ;
+ ["3"; "𝟛"; "③"; "⓷"; "𝟑"; ] ;
+ ["4"; "𝟜"; "④"; "⓸"; "𝟒"; ] ;
+ ["5"; "𝟝"; "⑤"; "⓹"; "𝟓"; ] ;
+ ["6"; "𝟞"; "⑥"; "⓺"; "𝟔"; ] ;
+ ["7"; "𝟟"; "⑦"; "⓻"; "𝟕"; ] ;
+ ["8"; "𝟠"; "⑧"; "⓼"; "𝟖"; "∞"; ] ;
+ ["9"; "𝟡"; "⑨"; "⓽"; "𝟗"; ] ;
  ]
 ;;