matita.cs.unibo.it Git - helm.git/history - helm/software/components/tactics/declarative.ml

]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/tactics/declarative.ml

[helm.git] / helm / software / components / tactics / declarative.ml

2007-06-13	Enrico Tassi	many changes:	blob \| commitdiff \| raw
2007-05-31	Claudio Sacerdoti...	Ferruccio has changed the semantics of the old ~pattern...	blob \| commitdiff \| raw \| diff to current
2007-05-17	Enrico Tassi	added a (for the moment) dummy field _subst to Proofeng...	blob \| commitdiff \| raw \| diff to current
2007-04-20	Claudio Sacerdoti...	The declarative rewriting step now tries auto timeout...	blob \| commitdiff \| raw \| diff to current
2007-03-16	Ferruccio Guidi	elim tactic: it needs two arguments, a term as well...	blob \| commitdiff \| raw \| diff to current
2007-03-13	Ferruccio Guidi	elim tactic: now takes a pattern instead of just a...	blob \| commitdiff \| raw \| diff to current
2007-03-01	Enrico Zoli	"by j let x : T such that P(x)" generalized to allow...	blob \| commitdiff \| raw \| diff to current
2007-01-10	Ferruccio Guidi	attributes now in the proof status: commit 2	blob \| commitdiff \| raw \| diff to current
2006-12-20	Claudio Sacerdoti...	New declarative tactic "we proceed by cases on t to...	blob \| commitdiff \| raw \| diff to current
2006-11-30	Claudio Sacerdoti...	New syntax and semantics for the rewriting steps that...	blob \| commitdiff \| raw \| diff to current
2006-11-29	Claudio Sacerdoti...	The rewritingstep declarative command now takes also...	blob \| commitdiff \| raw \| diff to current
2006-11-28	Claudio Sacerdoti...	Added a clear to rewritestep to speed up auto (by remov...	blob \| commitdiff \| raw \| diff to current
2006-11-27	Claudio Sacerdoti...	"the thesis becomes" now always performs a change.	blob \| commitdiff \| raw \| diff to current
2006-11-27	Claudio Sacerdoti...	Declarative language ported to new auto (with Universes).	blob \| commitdiff \| raw \| diff to current
2006-11-23	Andrea Asperti	Modifications to auto due to the introduction of the...	blob \| commitdiff \| raw \| diff to current
2006-11-14	Claudio Sacerdoti...	library=1 in obtain _ = _ by _.	blob \| commitdiff \| raw \| diff to current
2006-10-12	Claudio Sacerdoti...	Bug fixed: the conversion was done with the wront argum...	blob \| commitdiff \| raw \| diff to current
2006-10-10	Claudio Sacerdoti...	Implemented:	blob \| commitdiff \| raw \| diff to current
2006-10-03	maiorino	Some declarative tactics did not allow the "done" optio...	blob \| commitdiff \| raw \| diff to current
2006-10-03	Claudio Sacerdoti...	Syntax of paramodulation parameters changed.	blob \| commitdiff \| raw \| diff to current
2006-09-08	Claudio Sacerdoti...	Bug fixed: "by ... we proved ... that is equivalent...	blob \| commitdiff \| raw \| diff to current
2006-07-27	maiorino	Automation enabled for declarative proofs. Cool.	blob \| commitdiff \| raw \| diff to current
2006-07-27	maiorino	"that is equivalent to" and "or equivalently" implement...	blob \| commitdiff \| raw \| diff to current
2006-07-27	maiorino	All the declarative tactics now have a more or less...	blob \| commitdiff \| raw \| diff to current
2006-07-27	maiorino	Declarative tactics for rewriting steps, elimination...	blob \| commitdiff \| raw \| diff to current
2006-07-27	maiorino	New declarative commands (ast, pretty-printing and...	blob \| commitdiff \| raw \| diff to current
2006-07-12	Claudio Sacerdoti...	Missing copyright added to tactics/declarative.ml*	blob \| commitdiff \| raw \| diff to current
2006-07-11	maiorino	First experimental version of the declarative proof...	blob \| commitdiff \| raw \| diff to current

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom