X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2FlexerTHF.mll;h=4cbbb61bd25c9c9eef098d555054f549c0f7a120;hb=5c92c318030a05c766b3f6070dbd23589cbdee04;hp=6dc1d57957e1195ab231431ed63b24d4d314980e;hpb=fedecee9c4b10a2469c10fe09ec091d2dc6fc56a;p=helm.git

diff --git a/helm/software/components/tptp_grafite/lexerTHF.mll b/helm/software/components/tptp_grafite/lexerTHF.mll
index 6dc1d5795..4cbbb61bd 100644
--- a/helm/software/components/tptp_grafite/lexerTHF.mll
+++ b/helm/software/components/tptp_grafite/lexerTHF.mll
@@ -57,6 +57,9 @@ rule yylex = parse
    | '~' { NOT }
    | '=' { IEQ }
    | "=>" { IMPLY }
+   | "<=" { IMPLYLR }
+   | "<=>" { COIMPLY }
+   | "<~>" { XOR }
    | "!=" { NIEQ }
    | "!" { FORALL }
    | "?" { EXISTS }