slight refactoring in the proof of strong normalization

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

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 643f7c5ef4d2e7833626f60e7e7186730eda33fb..91b69fc6cef27905b8b62282dd3a88f1c65d7723 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1517,6 +1517,7 @@ let predefined_classes = [
  ["^"; "↑"; ] ;
  ["⇑"; "⇧"; "⬆"; ] ; 
  ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ;
+ ["⇕"; "⇳"; "⬍"; ];
  ["↔"; "⇔"; "⬄"; "⬌"; ] ; 
  ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ];
  ["_"; "↓"; "↙"; "⎽"; "⎼"; "⎻"; "⎺"; ];