From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 8 Apr 2010 17:44:46 +0000 (+0000)
Subject: support axioms
X-Git-Tag: make_still_working~2935
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c6de6147adbf650a444b81f0aaccc8cceeeb5b9b;p=helm.git

support axioms

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>
---

diff --git a/helm/software/components/tptp_grafite/mainTHF.ml b/helm/software/components/tptp_grafite/mainTHF.ml
index ece02f4a0..aa68fa61e 100644
--- a/helm/software/components/tptp_grafite/mainTHF.ml
+++ b/helm/software/components/tptp_grafite/mainTHF.ml
@@ -91,7 +91,7 @@ let _ =
            GA.NObj(floc,
             T.Theorem(`Definition,
              id,ty,Some body,`Regular)))):: aux tl
-      | A.ThfFormula(name,(A.Hypothesis|A.Assumption),term) :: tl -> 
+      | A.ThfFormula(name,(A.Axiom|A.Hypothesis|A.Assumption),term) :: tl -> 
          GA.Executable(floc,
           GA.NCommand(floc,
            GA.NObj(floc,