]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tptp_grafite/astTHF.ml
the edges must be quoted as well (not only the nodes)
[helm.git] / 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)