X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2FparserTHF.mly;h=99606a956ff0c8014825cba348faa15754f82d82;hb=7b8200f8aaf14195c0817e13234c712e7ab18eb6;hp=195b79f8de924c1f62ef96892190330de57503fe;hpb=f3c3059ab94266de1cdf7cbd1bbc62231d2f9a22;p=helm.git

diff --git a/helm/software/components/tptp_grafite/parserTHF.mly b/helm/software/components/tptp_grafite/parserTHF.mly
index 195b79f8d..99606a956 100644
--- a/helm/software/components/tptp_grafite/parserTHF.mly
+++ b/helm/software/components/tptp_grafite/parserTHF.mly
@@ -38,7 +38,10 @@ let unreserve k =
   %token IOR
   %token NIEQ
   %token IEQ
+  %token XOR
   %token IMPLY
+  %token IMPLYLR
+  %token COIMPLY
   %token PEQ
   %token DOT
   %token EOF
@@ -148,7 +151,11 @@ let unreserve k =
     | LPAREN term COLON term RPAREN { T.Cast ($2,$4) }
     | term TO term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
     | term IMPLY term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
+    | term IMPLYLR term { T.Binder (`Forall,(T.Ident("_",None),Some $3),$1) }
+    | term COIMPLY term { T.Appl [T.Symbol("Iff",0);$1;$3] }
+    | term XOR term { T.Appl [T.Symbol("Xor",0);$1;$3] }
     | term IEQ term { T.Appl [T.Symbol("Eq",0);$1;$3] }
+    | term NIEQ term { T.Appl [T.Symbol("NotEq",0);$1;$3] }
     | term IAND term { T.Appl [T.Symbol("And",0);$1;$3] }
     | term IOR term { T.Appl [T.Symbol("Or",0);$1;$3] }
     | NOT term { T.Appl [T.Symbol("Not",0);$2] }