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

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

2010-04-19	Andrea Asperti	Elimination of recursive inductive types leads to looping.	commit \| commitdiff \| tree
2010-04-19	Andrea Asperti	alpha_eq instead of pervasives.compare	commit \| commitdiff \| tree
2010-04-09	Andrea Asperti	apply_subst_context on statuses	commit \| commitdiff \| tree
2010-04-08	Andrea Asperti	Fixing indexing (commit parziale di Claudio?)	commit \| commitdiff \| tree
2010-03-31	Andrea Asperti	removed boh	commit \| commitdiff \| tree
2010-03-31	Andrea Asperti	Tracing mechanism for auto. Interface changed to solve...	commit \| commitdiff \| tree
2010-03-25	Andrea Asperti	More work	commit \| commitdiff \| tree
2010-03-25	Andrea Asperti	cosi va (se vi pare).	commit \| commitdiff \| tree
2010-03-25	Andrea Asperti	Conflict(?).	commit \| commitdiff \| tree
2010-03-25	Andrea Asperti	Extension of demod to arbtrary predicates (not just...	commit \| commitdiff \| tree
2010-03-24	Andrea Asperti	Computation of the trace.	commit \| commitdiff \| tree
2010-03-23	Andrea Asperti	One more case.	commit \| commitdiff \| tree
2010-03-23	Andrea Asperti	Readded eqf_2.	commit \| commitdiff \| tree
2010-03-23	Andrea Asperti	symmetric_eq -> sym_eq	commit \| commitdiff \| tree
2010-03-23	Andrea Asperti	Re-proved an axiom	commit \| commitdiff \| tree
2010-03-23	Andrea Asperti	Commented a few lemmas (copies).	commit \| commitdiff \| tree
2010-03-23	Andrea Asperti	Fixed a few bugs	commit \| commitdiff \| tree
2010-03-23	Andrea Asperti	"flat" function (subst unfolding)	commit \| commitdiff \| tree
2010-03-23	Andrea Asperti	Keeping only lift_aux e subst_aux (renamed to lift...	commit \| commitdiff \| tree
2010-03-23	Andrea Asperti	Moved compare in a different file.	commit \| commitdiff \| tree
2010-03-18	Andrea Asperti	Porting alla nuova def. di negazione	commit \| commitdiff \| tree
2010-03-18	Andrea Asperti	Nuova versione di not.	commit \| commitdiff \| tree
2010-03-18	Andrea Asperti	Printings removed.	commit \| commitdiff \| tree
2010-03-18	Andrea Asperti	Debugging disabled.	commit \| commitdiff \| tree
2010-03-18	Andrea Asperti	Debugging disabled.	commit \| commitdiff \| tree
2010-03-18	Andrea Asperti	New demodulation tactics (mostly for debugging purposes).	commit \| commitdiff \| tree
2010-03-18	Andrea Asperti	Exporting the demodulation function.	commit \| commitdiff \| tree
2010-03-18	Andrea Asperti	New option "demod" for auto.	commit \| commitdiff \| tree
2010-03-18	Andrea Asperti	Porting the new definition of equality.	commit \| commitdiff \| tree
2010-03-18	Andrea Asperti	app of app inside smart application.	commit \| commitdiff \| tree
2010-03-17	Andrea Asperti	qualche caso del lemma 5.2.11	commit \| commitdiff \| tree
2010-03-17	Andrea Asperti	Splitted gpts in two files.	commit \| commitdiff \| tree
2010-03-17	Andrea Asperti	Aggiornamento alla negazione.	commit \| commitdiff \| tree
2010-03-17	Andrea Asperti	Nuova definizione della negazione.	commit \| commitdiff \| tree
2010-03-12	Andrea Asperti	First version of PTS	commit \| commitdiff \| tree
2010-03-12	Andrea Asperti	New definition of negation	commit \| commitdiff \| tree
2010-03-12	Andrea Asperti	Subst was missing in perforate small (apparently, gty...	commit \| commitdiff \| tree
2010-03-12	Andrea Asperti	removed debug from the inteface	commit \| commitdiff \| tree
2010-03-04	Andrea Asperti	In line with the ml.	commit \| commitdiff \| tree
2010-03-04	Andrea Asperti	1. For smart application, we only perforate small terms...	commit \| commitdiff \| tree
2010-03-04	Andrea Asperti	Small changes for debugging	commit \| commitdiff \| tree
2010-03-04	Andrea Asperti	Fixed a bug in deep_eq: we generated new clauses but...	commit \| commitdiff \| tree
2010-03-04	Andrea Asperti	Corrected a bug relative to the application of substs...	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	Open goals fixed (it also returned closed goals).	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	Removed debug printings.	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	added lazy	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	Nuova versione di auto.	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	New proofs.	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	Wilmer's stuff for destruct.	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	(no commit message)	commit \| commitdiff \| tree
2010-02-19	Andrea Asperti	Added an implicit parameter to branch_tac to allow...	commit \| commitdiff \| tree
2010-02-16	Andrea Asperti	More theorems	commit \| commitdiff \| tree
2010-02-16	Andrea Asperti	Minor fixings.	commit \| commitdiff \| tree
2010-02-10	Andrea Asperti	addenda	commit \| commitdiff \| tree
2010-02-09	Andrea Asperti	Added a count_occurrences function.	commit \| commitdiff \| tree
2010-02-08	Andrea Asperti	Bug fixing.	commit \| commitdiff \| tree
2010-02-08	Andrea Asperti	Removed debug printings.	commit \| commitdiff \| tree
2010-02-08	Andrea Asperti	Some changes towards integration of setoid-rewriting.	commit \| commitdiff \| tree
2010-02-04	Andrea Asperti	Added count_occurrences.	commit \| commitdiff \| tree
2010-02-04	Andrea Asperti	Bug fixed: goto_top used to reset the status to the...	commit \| commitdiff \| tree
2010-02-02	Andrea Asperti	lists	commit \| commitdiff \| tree
2010-02-02	Andrea Asperti	Booleans	commit \| commitdiff \| tree
2010-02-02	Andrea Asperti	boolean arithmetics	commit \| commitdiff \| tree
2010-02-01	Andrea Asperti	minus	commit \| commitdiff \| tree
2010-02-01	Andrea Asperti	On the last goal at maxdepth we stop at the first solution.	commit \| commitdiff \| tree
2010-01-29	Andrea Asperti	minus in nat.ma	commit \| commitdiff \| tree
2010-01-29	Andrea Asperti	Nuova gestione della width.	commit \| commitdiff \| tree
2010-01-27	Andrea Asperti	le_arith	commit \| commitdiff \| tree
2010-01-27	Andrea Asperti	Unfolded exact letins during proof reconstruction.	commit \| commitdiff \| tree
2010-01-27	Andrea Asperti	Added a parameter no_implicit (default true) to choose...	commit \| commitdiff \| tree
2010-01-26	Andrea Asperti	le_arith	commit \| commitdiff \| tree
2010-01-21	Andrea Asperti	Esempio	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	New paramod tac.	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	Invocation of paramod	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	paramod_tac exported	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	Number notation for NG	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	Number notation for NG	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	Number notation for NG.	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	Keeping Implicit for refinement (instead of transforming...	commit \| commitdiff \| tree
2010-01-18	Andrea Asperti	Updating.	commit \| commitdiff \| tree
2010-01-11	Andrea Asperti	1. New paramodulation function	commit \| commitdiff \| tree
2010-01-11	Andrea Asperti	saturate cust be called with delta=0	commit \| commitdiff \| tree
2010-01-11	Andrea Asperti	Added is_equation	commit \| commitdiff \| tree
2010-01-11	Andrea Asperti	Debugging info	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	The body of constants is a reference, not the actual...	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	removed debugging info	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	rebuilding the library	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	rebuilding the library	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	rebuilding the library	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	applyS	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	refresh uri	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	Support for the new auto tactics //	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	Support for the new // tactics.	commit \| commitdiff \| tree
2010-01-08	Andrea Asperti	new reloc_subst (to avoid cyclic substitutions).	commit \| commitdiff \| tree
2009-12-21	Andrea Asperti	Refining with no expected type + unification seems...	commit \| commitdiff \| tree
2009-12-21	Andrea Asperti	Trying to be faster	commit \| commitdiff \| tree
2009-12-21	Andrea Asperti	Trying to be faster.	commit \| commitdiff \| tree
2009-12-18	Andrea Asperti	Final subst returned by superposition and passed around.	commit \| commitdiff \| tree
2009-12-18	Andrea Asperti	using = instead of alpha conversions. context metasenv...	commit \| commitdiff \| tree
2009-12-15	Andrea Asperti	eq_coerc for smart application.	commit \| commitdiff \| tree
next

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

RSS Atom