equal
deleted
inserted
replaced
31 gen_prec : bool, |
31 gen_prec : bool, |
32 gen_simp : bool} |
32 gen_simp : bool} |
33 |
33 |
34 datatype fool = Without_FOOL | With_FOOL |
34 datatype fool = Without_FOOL | With_FOOL |
35 datatype polymorphism = Monomorphic | Polymorphic |
35 datatype polymorphism = Monomorphic | Polymorphic |
36 datatype thf_choice = THF_Without_Choice | THF_With_Choice |
36 datatype thf_flavor = THF_Without_Choice | THF_With_Choice |
37 |
37 |
38 datatype atp_format = |
38 datatype atp_format = |
39 CNF | |
39 CNF | |
40 CNF_UEQ | |
40 CNF_UEQ | |
41 FOF | |
41 FOF | |
42 TFF of fool * polymorphism | |
42 TFF of fool * polymorphism | |
43 THF of fool * polymorphism * thf_choice | |
43 THF of fool * polymorphism * thf_flavor | |
44 DFG of polymorphism |
44 DFG of polymorphism |
45 |
45 |
46 datatype atp_formula_role = |
46 datatype atp_formula_role = |
47 Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture | |
47 Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture | |
48 Plain | Type_Role | Unknown |
48 Plain | Type_Role | Unknown |
189 gen_prec : bool, |
189 gen_prec : bool, |
190 gen_simp : bool} |
190 gen_simp : bool} |
191 |
191 |
192 datatype fool = Without_FOOL | With_FOOL |
192 datatype fool = Without_FOOL | With_FOOL |
193 datatype polymorphism = Monomorphic | Polymorphic |
193 datatype polymorphism = Monomorphic | Polymorphic |
194 datatype thf_choice = THF_Without_Choice | THF_With_Choice |
194 datatype thf_flavor = THF_Without_Choice | THF_With_Choice |
195 |
195 |
196 datatype atp_format = |
196 datatype atp_format = |
197 CNF | |
197 CNF | |
198 CNF_UEQ | |
198 CNF_UEQ | |
199 FOF | |
199 FOF | |
200 TFF of fool * polymorphism | |
200 TFF of fool * polymorphism | |
201 THF of fool * polymorphism * thf_choice | |
201 THF of fool * polymorphism * thf_flavor | |
202 DFG of polymorphism |
202 DFG of polymorphism |
203 |
203 |
204 datatype atp_formula_role = |
204 datatype atp_formula_role = |
205 Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture | |
205 Axiom | Definition | Lemma | Hypothesis | Conjecture | Negated_Conjecture | |
206 Plain | Type_Role | Unknown |
206 Plain | Type_Role | Unknown |