More work on concrete spaces.

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

diff --git a/helm/software/matita/predefined_virtuals.ml b/helm/software/matita/predefined_virtuals.ml
index e89af7d2b65907f3d6af77533f0be73955be62ce..4ca3542b6b8d256928ea6082f5ef2b97bf76ad46 100644 (file)
--- a/helm/software/matita/predefined_virtuals.ml
+++ b/helm/software/matita/predefined_virtuals.ml
@@ -714,7 +714,7 @@ let predefined_virtuals = [
  ["\\wedgeq"                                         ], "≙", [equivalence];
  ["\\veeeq"                                          ], "≚", [equivalence];
  ["\\trie"; "\\triangleq"                             ], "≜", [equivalence];
- ["\\def"                                            ], "≝", [equivalence];
+ ["\\def";":=" ], "≝", [equivalence];
  ["\\equest"; "\\questeq"                             ], "≟", [equivalence];
  ["\\ne"; "\\neq"; "\\NotEqual"                        ], "≠", [equivalence];
  ["\\equiv"; "\\Congruent"                            ], "≡", [equivalence];
@@ -1505,10 +1505,11 @@ let predefined_classes = [
  ["→"; "⇉"; "⇒"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; "⥤"; "⥰"; ] ;
  ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; ];
  ["_" ; "⎽"; "⎼"; "⎻"; "⎺"; ];
- ["<"; "≺"; "≮"; "⊀"; ] ;
+ ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; ] ;
  ["□"; "◽"; "▪"; "◾"; ];
- ["â\97\8b"; "â\88\98";  "ø"; ] ;
+ ["â\88\98";  "ø"; "â\97\8b"; ] ;
  ["◊"; "♢"; "⧫"; "♦"; ];
+ [">"; "〉"; "»"; ];       
  ["a"; "α"; "𝕒"; ] ;
  ["A"; "ℵ"; "𝔸"; ] ;
  ["b"; "β"; "ß"; "𝕓"; ] ;
@@ -1561,6 +1562,16 @@ let predefined_classes = [
  ["Y"; "ϒ"; "𝕐"; ] ;
  ["z"; "ζ"; "𝕫"; ] ;
  ["Z"; "ℨ"; "ℤ"; ] ;
+ ["0"; "𝟘"; ] ;
+ ["1"; "𝟙"; ] ;
+ ["2"; "𝟚"; ] ;
+ ["3"; "𝟛"; ] ;
+ ["4"; "𝟜"; ] ;
+ ["5"; "𝟝"; ] ;
+ ["6"; "𝟞"; ] ;
+ ["7"; "𝟟"; ] ;
+ ["8"; "𝟠"; ] ;
+ ["9"; "𝟡"; ] ;
  ]
 ;;