helm/software/components/tptp_grafite/astTHF.ml

   1 type role =
   2   Axiom
   3 | Hypothesis
   4 | Definition
   5 | Assumption
   6 | Lemma
   7 | Theorem
   8 | Conjecture
   9 | Negated_conjecture
  10 | Lemma_conjecture
  11 | Plain
  12 | Fi_domain
  13 | Fi_functors
  14 | Fi_predicates
  15 | Type
  16 | Unknown
  17
  18
  19 type ast =
  20   | ThfFormula of string * role * CicNotationPt.term
  21   | ThfDefinition of string * string * CicNotationPt.term
  22   | ThfType of string * string * CicNotationPt.term
  23   | Comment of string
  24   | Inclusion of string * (string list)