]> matita.cs.unibo.it Git - helm.git/commitdiff
an addition ...
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 28 Oct 2012 14:39:27 +0000 (14:39 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sun, 28 Oct 2012 14:39:27 +0000 (14:39 +0000)
matita/matita/predefined_virtuals.ml

index b51681d92d162db45eab6f31ac8d71934bac582f..4d86409b70147f19adb3aa42e3cc93c25c7952d6 100644 (file)
@@ -1524,8 +1524,8 @@ let predefined_classes = [
  ["}"; "❵"; "⦄" ] ;
  ["□"; "◽"; "▪"; "◾"; ];
  ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ;
- [">"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ;
- ["≥"; "≽"; ]; 
+ [">"; "â­\83"; "â\8cª"; "»"; "â\9d­"; "â\9d¯"; "â\9d±"; "â\96¸"; "â\96º"; "â\96¶"; ] ;
+ ["≥"; "≽"; "⥸"; ]; 
  ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ;
  ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ;
  ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ;