]> matita.cs.unibo.it Git - helm.git/commitdiff
support axioms
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 8 Apr 2010 17:44:46 +0000 (17:44 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 8 Apr 2010 17:44:46 +0000 (17:44 +0000)
From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

helm/software/components/tptp_grafite/mainTHF.ml

index ece02f4a0cc2d66b672f8d3fd4d7e6eba676d1b6..aa68fa61eb738e7909e17e9abc5a5fd0cf2e842a 100644 (file)
@@ -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,