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

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

2010-04-08	Andrea Asperti	Fixing indexing (commit parziale di Claudio?)	commit \| commitdiff \| tree \| snapshot
2010-04-07	Enrico Tassi	THF parser for TPTP	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	Not is now inductive.	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	Use the inversion!	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	Bug fixed: the current equation is not always the last...	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	- inversion principles are now generated also for co...	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	More debugging info from print_tac.	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	Implicit and UserInput were printed incorrectly.	commit \| commitdiff \| tree \| snapshot
2010-03-31	Claudio Sacerdoti...	ninversion	commit \| commitdiff \| tree \| snapshot
2010-03-31	Andrea Asperti	removed boh	commit \| commitdiff \| tree \| snapshot
2010-03-31	Wilmer Ricciotti	Added test file for inversion in ng matita.	commit \| commitdiff \| tree \| snapshot
2010-03-31	Andrea Asperti	Tracing mechanism for auto. Interface changed to solve...	commit \| commitdiff \| tree \| snapshot
2010-03-26	Claudio Sacerdoti...	Good definition found.	commit \| commitdiff \| tree \| snapshot
2010-03-26	Claudio Sacerdoti...	(Co)Inductively Generated Formal Topologies (not only...	commit \| commitdiff \| tree \| snapshot
2010-03-25	Matthias Puech	patched the definition of locate, advances in locate_ad...	commit \| commitdiff \| tree \| snapshot
2010-03-25	Wilmer Ricciotti	Z.ma updated to reflect changes in the logical Not...	commit \| commitdiff \| tree \| snapshot
2010-03-25	Matthias Puech	Automation problem	commit \| commitdiff \| tree \| snapshot
2010-03-25	Andrea Asperti	More work	commit \| commitdiff \| tree \| snapshot
2010-03-25	Andrea Asperti	cosi va (se vi pare).	commit \| commitdiff \| tree \| snapshot
2010-03-25	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2010-03-25	Andrea Asperti	Conflict(?).	commit \| commitdiff \| tree \| snapshot
2010-03-25	Andrea Asperti	Extension of demod to arbtrary predicates (not just...	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	Nice examples for automation (that fails).	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	Simplified proof after pattern fix	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	"Not" is no longer a definition	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	The precedence of ^-1 has changed.	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	Equality has one right parameter and thus it's eliminat...	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	Axioms were not indexed.	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	Axioms were not indexed.	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2010-03-24	Claudio Sacerdoti...	Real numbers as co-inductive streams of digits (overlap...	commit \| commitdiff \| tree \| snapshot
2010-03-24	Andrea Asperti	Computation of the trace.	commit \| commitdiff \| tree \| snapshot
2010-03-23	Matthias Puech	typo in a proof	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	One more case.	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	Readded eqf_2.	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	symmetric_eq -> sym_eq	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	Re-proved an axiom	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	Commented a few lemmas (copies).	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	Fixed a few bugs	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	"flat" function (subst unfolding)	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	Keeping only lift_aux e subst_aux (renamed to lift...	commit \| commitdiff \| tree \| snapshot
2010-03-23	Andrea Asperti	Moved compare in a different file.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Matthias Puech	Downgrading level of infix notations involving \sup.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	Porting alla nuova def. di negazione	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	Nuova versione di not.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	Printings removed.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	Debugging disabled.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	Debugging disabled.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	New demodulation tactics (mostly for debugging purposes).	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	Exporting the demodulation function.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	New option "demod" for auto.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	Porting the new definition of equality.	commit \| commitdiff \| tree \| snapshot
2010-03-18	Claudio Sacerdoti...	Do not index examples (concrete syntax: nremark).	commit \| commitdiff \| tree \| snapshot
2010-03-18	Claudio Sacerdoti...	nremark => `Example (not to be indexed)	commit \| commitdiff \| tree \| snapshot
2010-03-18	Andrea Asperti	app of app inside smart application.	commit \| commitdiff \| tree \| snapshot
2010-03-17	Ferruccio Guidi	dr	commit \| commitdiff \| tree \| snapshot
2010-03-17	Andrea Asperti	qualche caso del lemma 5.2.11	commit \| commitdiff \| tree \| snapshot
2010-03-17	Claudio Sacerdoti...	OCaml's inferred type simplified.	commit \| commitdiff \| tree \| snapshot
2010-03-17	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2010-03-17	Andrea Asperti	Splitted gpts in two files.	commit \| commitdiff \| tree \| snapshot
2010-03-17	Andrea Asperti	Aggiornamento alla negazione.	commit \| commitdiff \| tree \| snapshot
2010-03-17	Andrea Asperti	Nuova definizione della negazione.	commit \| commitdiff \| tree \| snapshot
2010-03-16	Claudio Sacerdoti...	Comparison of two applications with a different number...	commit \| commitdiff \| tree \| snapshot
2010-03-16	Claudio Sacerdoti...	1) intros cleans up the cache (because the context...	commit \| commitdiff \| tree \| snapshot
2010-03-16	Claudio Sacerdoti...	refreshing of inferred type was missing	commit \| commitdiff \| tree \| snapshot
2010-03-16	Claudio Sacerdoti...	...	commit \| commitdiff \| tree \| snapshot
2010-03-12	Andrea Asperti	First version of PTS	commit \| commitdiff \| tree \| snapshot
2010-03-12	Andrea Asperti	New definition of negation	commit \| commitdiff \| tree \| snapshot
2010-03-12	Andrea Asperti	Subst was missing in perforate small (apparently, gty...	commit \| commitdiff \| tree \| snapshot
2010-03-12	Andrea Asperti	removed debug from the inteface	commit \| commitdiff \| tree \| snapshot
2010-03-04	Andrea Asperti	In line with the ml.	commit \| commitdiff \| tree \| snapshot
2010-03-04	Andrea Asperti	1. For smart application, we only perforate small terms...	commit \| commitdiff \| tree \| snapshot
2010-03-04	Andrea Asperti	Small changes for debugging	commit \| commitdiff \| tree \| snapshot
2010-03-04	Andrea Asperti	Fixed a bug in deep_eq: we generated new clauses but...	commit \| commitdiff \| tree \| snapshot
2010-03-04	Andrea Asperti	Corrected a bug relative to the application of substs...	commit \| commitdiff \| tree \| snapshot
2010-03-02	Wilmer Ricciotti	Added reverse rewriting principle in Type[0].	commit \| commitdiff \| tree \| snapshot
2010-03-02	Wilmer Ricciotti	Some integrations to the ng library.	commit \| commitdiff \| tree \| snapshot
2010-03-02	Wilmer Ricciotti	Added syntax for ninversion tactic (still experimental).	commit \| commitdiff \| tree \| snapshot
2010-03-02	Enrico Tassi	Constants are indexed using the Reference, not the...	commit \| commitdiff \| tree \| snapshot
2010-03-01	Wilmer Ricciotti	Fixed a bug in the unification, which prevented some...	commit \| commitdiff \| tree \| snapshot
2010-02-25	Ferruccio Guidi	-bugfix in the "profile" entry	commit \| commitdiff \| tree \| snapshot
2010-02-25	Ferruccio Guidi	- pipeline support for generated entities in text mode...	commit \| commitdiff \| tree \| snapshot
2010-02-25	Wilmer Ricciotti	Minimal example in Z showing a problem in the nnormaliz...	commit \| commitdiff \| tree \| snapshot
2010-02-24	Ferruccio Guidi	- a couple of new entities	commit \| commitdiff \| tree \| snapshot
2010-02-23	Ferruccio Guidi	- the text model now supports invocations of the entity...	commit \| commitdiff \| tree \| snapshot
2010-02-22	Ferruccio Guidi	- we completed the text parser fixing the syntactic...	commit \| commitdiff \| tree \| snapshot
2010-02-21	Ferruccio Guidi	- we added some syntactic sugar in the text parser	commit \| commitdiff \| tree \| snapshot
2010-02-20	Ferruccio Guidi	- we implemented the hierarchy and sort names declarati...	commit \| commitdiff \| tree \| snapshot
2010-02-19	Andrea Asperti	Open goals fixed (it also returned closed goals).	commit \| commitdiff \| tree \| snapshot
2010-02-19	Ferruccio Guidi	- we added a parser for lambda-delta textual syntax...	commit \| commitdiff \| tree \| snapshot
2010-02-19	Andrea Asperti	Removed debug printings.	commit \| commitdiff \| tree \| snapshot
2010-02-19	Andrea Asperti	added lazy	commit \| commitdiff \| tree \| snapshot
2010-02-19	Andrea Asperti	Nuova versione di auto.	commit \| commitdiff \| tree \| snapshot
2010-02-19	Andrea Asperti	New proofs.	commit \| commitdiff \| tree \| snapshot
2010-02-19	Andrea Asperti	Wilmer's stuff for destruct.	commit \| commitdiff \| tree \| snapshot
2010-02-19	Andrea Asperti	(no commit message)	commit \| commitdiff \| tree \| snapshot
2010-02-19	Andrea Asperti	Added an implicit parameter to branch_tac to allow...	commit \| commitdiff \| tree \| snapshot
2010-02-16	Andrea Asperti	More theorems	commit \| commitdiff \| tree \| snapshot
next

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

RSS Atom