]> matita.cs.unibo.it Git - helm.git/history - components/tactics/paramodulation/equality.ml
New version of deep_subsumption
[helm.git] / components / tactics / paramodulation / equality.ml
2006-05-05 Andrea AspertiNew version of deep_subsumption
2006-05-04 Enrico Tassigoal demodulated with new
2006-05-04 Enrico Tassinew pp function for proofs
2006-05-03 Enrico Tassimore transitivity on proofs
2006-04-26 Andrea AspertiBuild_proof_goal does not return the metasenv any more.
2006-04-26 Enrico Tassiadded a new type for proofs.