From 28677364f03d66dfacfe67c5b1b6c40136fbd8f0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 13 Sep 2009 21:01:55 +0000 Subject: [PATCH] some more letters --- helm/software/matita/predefined_virtuals.ml | 104 ++++++++++---------- 1 file changed, 52 insertions(+), 52 deletions(-) diff --git a/helm/software/matita/predefined_virtuals.ml b/helm/software/matita/predefined_virtuals.ml index a263c03bd..31d6e8499 100644 --- a/helm/software/matita/predefined_virtuals.ml +++ b/helm/software/matita/predefined_virtuals.ml @@ -1510,58 +1510,58 @@ let predefined_classes = [ ["□"; "◽"; "▪"; "◾"; ]; ["◊"; "♢"; "⧫"; "♦"; ]; [">"; "〉"; "»"; ]; - ["a"; "α"; "𝕒"; ] ; - ["A"; "ℵ"; "𝔸"; ] ; - ["b"; "β"; "ß"; "𝕓"; ] ; - ["B"; "ℶ"; "ℬ"; "𝔹"; ] ; - ["c"; "𝕔"; ] ; - ["C"; "ℭ"; "∁"; ] ; - ["d"; "δ"; "∂"; "𝕕"; "ⅆ"; ] ; - ["D"; "Δ"; "𝔻"; "ⅅ"; ] ; - ["e"; "ɛ"; "ε"; "ϵ"; "Є"; "ℯ"; "𝕖"; "ⅇ"; ] ; - ["E"; "ℰ"; "𝔼"; ] ; - ["f"; "φ"; "ψ"; "ϕ"; "⨍"; "𝕗"; ] ; - ["F"; "Φ"; "Ψ"; "ℱ"; "𝔽"; ] ; - ["g"; "γ"; "ℊ"; "𝕘"; ] ; - ["G"; "Γ"; "𝔾"; ] ; - ["h"; "η"; "ℌ"; "ℎ"; "𝕙"; ] ; - ["H"; "ℋ"; "ℍ"; ] ; - ["i"; "ι"; "ℐ"; "𝕚"; "ⅈ"; ] ; - ["I"; "𝕀"; ] ; - ["j"; "𝕛"; ] ; - ["J"; "Ј"; "𝕁"; ] ; - ["k"; "κ"; "𝕜"; ] ; - ["K"; "𝕂"; ] ; - ["l"; "λ"; "𝕝"; ] ; - ["L"; "Λ"; "𝕃"; ] ; - ["m"; "μ"; "𝕞"; ] ; - ["M"; "ℳ"; "𝕄"; ] ; - ["n"; "𝕟"; ] ; - ["N"; "ℕ"; "№"; ] ; - ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "ø"; "○"; ] ; - ["O"; "Θ"; "𝕆"; ] ; - ["p"; "π"; "𝕡"; ] ; - ["P"; "Π"; "℘"; "ℙ"; ] ; - ["q"; "𝕢"; ] ; - ["Q"; "ℚ"; ] ; - ["r"; "ρ"; "ϱ"; "𝕣"; ] ; - ["R"; "ℛ"; "ℜ"; "ℝ"; ] ; - ["s"; "σ"; "ς"; "𝕤"; ] ; - ["S"; "Σ"; "𝕊"; ] ; - ["t"; "τ"; "𝕥"; ] ; - ["T"; "𝕋"; ] ; - ["u"; "𝕦"; ] ; - ["U"; "𝕌"; ] ; - ["v"; "ν"; "𝕧"; ] ; - ["V"; "𝕍"; ] ; - ["w"; "ω"; "𝕨"; ] ; - ["W"; "Ω"; "𝕎"; ] ; - ["x"; "ξ"; "χ"; "ϰ"; "𝕩"; ] ; - ["X"; "Ξ"; "𝕏"; ] ; - ["y"; "υ"; "𝕪"; ] ; - ["Y"; "ϒ"; "𝕐"; ] ; - ["z"; "ζ"; "𝕫"; ] ; - ["Z"; "ℨ"; "ℤ"; ] ; + ["a"; "α"; "𝕒"; "𝐚";] ; + ["A"; "ℵ"; "𝔸"; "𝐀";] ; + ["b"; "β"; "ß"; "𝕓"; "𝐛"; ] ; + ["B"; "ℶ"; "ℬ"; "𝔹"; "𝐁";] ; + ["c"; "𝕔"; "𝐜";] ; + ["C"; "ℭ"; "∁"; "𝐂";] ; + ["d"; "δ"; "∂"; "𝕕"; "ⅆ"; "𝐝";] ; + ["D"; "Δ"; "𝔻"; "ⅅ"; "𝐃";] ; + ["e"; "ɛ"; "ε"; "ϵ"; "Є"; "ℯ"; "𝕖"; "ⅇ"; "𝐞";] ; + ["E"; "ℰ"; "𝔼"; "𝐄";] ; + ["f"; "φ"; "ψ"; "ϕ"; "⨍"; "𝕗"; "𝐟";] ; + ["F"; "Φ"; "Ψ"; "ℱ"; "𝔽"; "𝐅";] ; + ["g"; "γ"; "ℊ"; "𝕘"; "𝐠";] ; + ["G"; "Γ"; "𝔾"; "𝐆";] ; + ["h"; "η"; "ℌ"; "ℎ"; "𝕙"; "𝐡";] ; + ["H"; "ℋ"; "ℍ"; "𝐇";] ; + ["i"; "ι"; "ℐ"; "𝕚"; "ⅈ"; "𝐢";] ; + ["I"; "𝕀"; "𝐈";] ; + ["j"; "𝕛"; "𝐣";] ; + ["J"; "Ј"; "𝕁"; "𝐉";] ; + ["k"; "κ"; "𝕜"; "𝐤";] ; + ["K"; "𝕂"; "𝐊";] ; + ["l"; "λ"; "𝕝"; "𝐥";] ; + ["L"; "Λ"; "𝕃"; "𝐋";] ; + ["m"; "μ"; "𝕞"; "𝐦";] ; + ["M"; "ℳ"; "𝕄"; "𝐌"; ] ; + ["n"; "𝕟"; "𝐧";] ; + ["N"; "ℕ"; "№"; "𝐍";] ; + ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "ø"; "○"; "𝐨";] ; + ["O"; "Θ"; "𝕆"; "𝐎";] ; + ["p"; "π"; "𝕡"; "𝐩";] ; + ["P"; "Π"; "℘"; "ℙ"; "𝐏"; ] ; + ["q"; "𝕢"; "𝐪";] ; + ["Q"; "ℚ"; "𝐐";] ; + ["r"; "ρ"; "ϱ"; "𝕣"; "𝐫";] ; + ["R"; "ℛ"; "ℜ"; "ℝ"; "𝐑";] ; + ["s"; "σ"; "ς"; "𝕤"; "𝐬";] ; + ["S"; "Σ"; "𝕊"; "𝐒";] ; + ["t"; "τ"; "𝕥"; "𝐭";] ; + ["T"; "𝕋"; "𝐓";] ; + ["u"; "𝕦"; "𝐮";] ; + ["U"; "𝕌"; "𝐔"; ] ; + ["v"; "ν"; "𝕧"; "𝐯";] ; + ["V"; "𝕍"; "𝐕";] ; + ["w"; "ω"; "𝕨"; "𝐰";] ; + ["W"; "Ω"; "𝕎"; "𝐖";] ; + ["x"; "ξ"; "χ"; "ϰ"; "𝕩"; "𝐱";] ; + ["X"; "Ξ"; "𝕏";"𝐗"; ] ; + ["y"; "υ"; "𝕪"; "𝐲";] ; + ["Y"; "ϒ"; "𝕐"; "𝐘";] ; + ["z"; "ζ"; "𝕫"; "𝐳";] ; + ["Z"; "ℨ"; "ℤ"; "𝐙";] ; ["0"; "𝟘"; ] ; ["1"; "𝟙"; ] ; ["2"; "𝟚"; ] ; -- 2.39.2