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

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

2009-06-30	denes	Enabled age selection (ratio 1/5)	commit \| commitdiff \| tree
2009-06-29	denes	First attempt for refined goal selection strategy	commit \| commitdiff \| tree
2009-06-29	denes	Implemented orphan murdering technique	commit \| commitdiff \| tree
2009-06-26	denes	Implemented orphan murder test (clauses are not discarded...	commit \| commitdiff \| tree
2009-06-25	denes	Various fixes	commit \| commitdiff \| tree
2009-06-25	denes	Now using age selection	commit \| commitdiff \| tree
2009-06-25	denes	Fixed is_identity for facts	commit \| commitdiff \| tree
2009-06-25	denes	Fixed insertion of passive clauses	commit \| commitdiff \| tree
2009-06-24	denes	Removed debug printing	commit \| commitdiff \| tree
2009-06-24	denes	Now inserting hypothesis and goal with zero weight	commit \| commitdiff \| tree
2009-06-24	denes	Extended is_identity test	commit \| commitdiff \| tree
2009-06-24	denes	Implemented check for duplicates (in goals)	commit \| commitdiff \| tree
2009-06-23	denes	Removed old debugging assertion	commit \| commitdiff \| tree
2009-06-23	denes	Removed debug printing raising Failure	commit \| commitdiff \| tree
2009-06-23	denes	Removed debug printing	commit \| commitdiff \| tree
2009-06-23	denes	Rewrote the main loop for paramodulation	commit \| commitdiff \| tree
2009-06-23	denes	Fixed nasty bug in maxvar updating	commit \| commitdiff \| tree
2009-06-22	denes	Added more precise time information	commit \| commitdiff \| tree
2009-06-22	denes	Added problems from CASC 208	commit \| commitdiff \| tree
2009-06-22	denes	Regenerated problems with corrected tptp2grafite	commit \| commitdiff \| tree
2009-06-22	denes	Corrected proof visiting (topological sort)	commit \| commitdiff \| tree
2009-06-22	denes	Small debugging in tptp2grafite	commit \| commitdiff \| tree
2009-06-18	denes	Added ntry and nassumption tactics	commit \| commitdiff \| tree
2009-06-18	denes	Fixed stupid path	commit \| commitdiff \| tree
2009-06-18	denes	Added script useful for running benchmarks	commit \| commitdiff \| tree
2009-06-18	denes	Changed parenthesis to optional around letin ident...	commit \| commitdiff \| tree
2009-06-18	denes	Fixed wrong types in proof terms	commit \| commitdiff \| tree
2009-06-17	denes	Added optionnal one pass simplification (instead of...	commit \| commitdiff \| tree
2009-06-12	denes	Implemented keep_simplified.	commit \| commitdiff \| tree
2009-06-11	denes	Active goals are now demodulated after selecting a...	commit \| commitdiff \| tree
2009-06-10	denes	Extended the equality case to non ground terms	commit \| commitdiff \| tree
2009-06-09	denes	Optimized weigths comparison, removed normalization	commit \| commitdiff \| tree
2009-06-09	denes	Implemented substitution application and concatenation	commit \| commitdiff \| tree
2009-06-05	denes	First tests for paramodulation (pretty printer, unification)	commit \| commitdiff \| tree
2009-06-05	denes	Fix : wrong exception was catch in apply_subst	commit \| commitdiff \| tree
2009-06-04	denes	First pretty printing functions	commit \| commitdiff \| tree
2009-06-01	denes	First implementation of unification on foterms	commit \| commitdiff \| tree
2009-06-01	denes	First functions on substitutions for unification	commit \| commitdiff \| tree
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
2006-01-11	marangon	Code clean up.	commit \| commitdiff \| tree
2005-12-15	marangon	New tactic: inversion.	commit \| commitdiff \| tree
2005-12-15	marangon	New tactic: inversion.	commit \| commitdiff \| tree
2005-12-15	marangon	...	commit \| commitdiff \| tree
2005-12-15	marangon	added -I ../.. (for coq.ma)	commit \| commitdiff \| tree
next

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

RSS Atom