matita.cs.unibo.it Git - helm.git/search

]> matita.cs.unibo.it Git - helm.git/search

2007-10-14	Cristian Armentano	Theorem sigma_p_knm changed into generic_iter_p_knm.	commit \| commitdiff \| tree
2007-09-20	Cristian Armentano	Further simplifications to the main theorem about Euler...	commit \| commitdiff \| tree
2007-09-19	Cristian Armentano	* Some simplifications to theorem in file totient1.ma.	commit \| commitdiff \| tree
2007-09-18	Cristian Armentano	some theorems have been moved to more appropriate files...	commit \| commitdiff \| tree
2007-09-17	Cristian Armentano	temporary changes, before the complete cancellation...	commit \| commitdiff \| tree
2007-09-17	Cristian Armentano	simplified version of a theorem.	commit \| commitdiff \| tree
2007-09-11	Cristian Armentano	some theorem names changed.	commit \| commitdiff \| tree
2007-09-10	Cristian Armentano	other simplifications.	commit \| commitdiff \| tree
2007-09-09	Cristian Armentano	other simplifications.	commit \| commitdiff \| tree
2007-09-07	Cristian Armentano	some simplifications.	commit \| commitdiff \| tree
2007-09-06	Cristian Armentano	Some simplifications.	commit \| commitdiff \| tree
2007-08-16	Cristian Armentano	little change to theorem eq_gcd_times_times_eqv_times_gcd	commit \| commitdiff \| tree
2007-07-30	Cristian Armentano	renamed generic_sigma_p.ma to generic_iter_p.ma	commit \| commitdiff \| tree
2007-06-30	Cristian Armentano	New definition of Euler's totient function.	commit \| commitdiff \| tree
2007-06-29	Cristian Armentano	generic version, specializing generic_sigma_p.ma	commit \| commitdiff \| tree
2007-06-29	Cristian Armentano	generic version	commit \| commitdiff \| tree
2007-06-29	Cristian Armentano	theorems about sigma_p proved using sigma_p_gen	commit \| commitdiff \| tree
2007-06-27	Cristian Armentano	new gcd properties, and theorems for totient, and theorems...	commit \| commitdiff \| tree
2007-06-26	Cristian Armentano	(no commit message)	commit \| commitdiff \| tree
2007-06-26	Cristian Armentano	generic sommatory.	commit \| commitdiff \| tree
2007-05-18	lzingare	added alternative implementation for hMysql relying	commit \| commitdiff \| tree
2007-04-20	Cristian Armentano	changed base uri	commit \| commitdiff \| tree
2007-04-20	Cristian Armentano	initial import	commit \| commitdiff \| tree
2007-03-01	Enrico Zoli	"by j let x : T such that P(x)" generalized to allow...	commit \| commitdiff \| tree
2007-02-20	notin	small fix to make it compile again	commit \| commitdiff \| tree
2007-01-17	Enrico Zoli	This is the roadmap of the constructive proof of Lebesgue...	commit \| commitdiff \| tree
2006-12-15	Enrico Zoli	Up to definition of limsup as liminf computed on the...	commit \| commitdiff \| tree
2006-12-15	Enrico Zoli	Fatou lemma achieved (up to a few more axioms here...	commit \| commitdiff \| tree
2006-11-14	maiorino	New: on-line help for declarative tactics (first version).	commit \| commitdiff \| tree
2006-11-10	Enrico Zoli	Dama: up to L-spaces and the proof (completed up to...	commit \| commitdiff \| tree
2006-11-06	Enrico Zoli	More work on groups, real numbers and integration algebras.	commit \| commitdiff \| tree
2006-11-03	Enrico Zoli	Integration f_algebras declassed.	commit \| commitdiff \| tree
2006-11-03	Enrico Zoli	Up to absolute value	commit \| commitdiff \| tree
2006-11-03	Enrico Zoli	Up to max (up to a bug).	commit \| commitdiff \| tree
2006-10-31	Enrico Zoli	We begin to play the real game: we have defined real...	commit \| commitdiff \| tree
2006-10-31	Enrico Zoli	Integration_algebras.ma split into 6 different files.	commit \| commitdiff \| tree
2006-10-31	Enrico Zoli	Syntax changed (to be changed back) for left parameters...	commit \| commitdiff \| tree
2006-10-24	Enrico Zoli	Added unit to rings.	commit \| commitdiff \| tree
2006-10-24	Enrico Zoli	More coercions added in the algebraic hierarchy.	commit \| commitdiff \| tree
2006-10-24	Enrico Zoli	Up to f_algebras.	commit \| commitdiff \| tree
2006-10-20	Enrico Zoli	Up to f_algebras.	commit \| commitdiff \| tree
2006-10-20	Enrico Zoli	1. developed up to algebras	commit \| commitdiff \| tree
2006-10-20	Enrico Zoli	Serious bug fixed: without a Lazy.force the user obtained...	commit \| commitdiff \| tree
2006-10-16	Enrico Zoli	Beginning of the development of integration algebras.	commit \| commitdiff \| tree
2006-10-12	acciavat	auto => auto new.	commit \| commitdiff \| tree
2006-10-12	acciavat	Manual porting of CoRN to Matita.	commit \| commitdiff \| tree
2006-10-03	maiorino	Some declarative tactics did not allow the "done" option...	commit \| commitdiff \| tree
2006-07-27	maiorino	Automation enabled for declarative proofs. Cool.	commit \| commitdiff \| tree
2006-07-27	maiorino	"that is equivalent to" and "or equivalently" implemented...	commit \| commitdiff \| tree
2006-07-27	maiorino	All the declarative tactics now have a more or less...	commit \| commitdiff \| tree
2006-07-27	maiorino	Declarative tactics for rewriting steps, elimination...	commit \| commitdiff \| tree
2006-07-27	maiorino	Notation for the existential quantifier moved to core_notati...	commit \| commitdiff \| tree
2006-07-27	maiorino	New declarative commands (ast, pretty-printing and...	commit \| commitdiff \| tree
2006-07-11	maiorino	First experimental version of the declarative proof...	commit \| commitdiff \| tree
2006-03-10	marangon	Added inversion principle creation for inductive predicates.	commit \| commitdiff \| tree
2006-03-10	marangon	Inversion code cleaning.	commit \| commitdiff \| tree
2006-03-03	marangon	PP of Refine.RefineFailure.	commit \| commitdiff \| tree

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

RSS Atom