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

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

projects / helm.git / history

summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next

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

2008-05-26	Enrico Tassi	new, more rigid syntax, for auto_params affecting the...	blob \| commitdiff \| raw
2008-03-20	Enrico Tassi	changed auto_tac params type and all derivate tactics...	blob \| commitdiff \| raw \| diff to current
2007-07-04	Claudio Sacerdoti...	1. "by proof" now allowed as a justification in equalit...	blob \| commitdiff \| raw \| diff to current
2007-05-18	lzingare	added alternative implementation for hMysql relying	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
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-27	Claudio Sacerdoti...	Declarative language ported to new auto (with Universes).	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-07-27	maiorino	Automation enabled for declarative proofs. Cool.	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.