(*query to obtain all the constants in the hypothesis of the theorem*)
let query =
"select h_occurrence from refObj where source='"^uri^
"' and (h_position="^main_hypothesis^" or h_position="^in_hypothesis^
"or h_position="^main_conclusion^" or h_position="^in_conclusion^")" in
(*query to obtain all the constants in the hypothesis of the theorem*)
let query =
"select h_occurrence from refObj where source='"^uri^
"' and (h_position="^main_hypothesis^" or h_position="^in_hypothesis^
"or h_position="^main_conclusion^" or h_position="^in_conclusion^")" in
const, the set of the costants of the proof *)
let filter_new_constants (conn:Mysql.dbd) const (_,uri) =
let hyp = hyp_const conn uri in
const, the set of the costants of the proof *)
let filter_new_constants (conn:Mysql.dbd) const (_,uri) =
let hyp = hyp_const conn uri in