matita.cs.unibo.it Git - helm.git/history - helm/matita/matitaEngine.ml

]> matita.cs.unibo.it Git - helm.git/history - helm/matita/matitaEngine.ml

[helm.git] / helm / matita / matitaEngine.ml

2005-07-13	Enrico Tassi	matitamake stuff:	blob \| commitdiff \| raw
2005-07-11	Enrico Tassi	added a flag to do the check of alredy-proved-theorem	blob \| commitdiff \| raw \| diff to current
2005-07-08	Enrico Tassi	added variant thm flavour	blob \| commitdiff \| raw \| diff to current
2005-07-08	Enrico Tassi	added query	blob \| commitdiff \| raw \| diff to current
2005-07-07	Claudio Sacerdoti...	1. Warnings are now printed in orange (yellow was unvis...	blob \| commitdiff \| raw \| diff to current
2005-07-07	Andrea Asperti	Raising an error on a bad theorem name.	blob \| commitdiff \| raw \| diff to current
2005-07-06	Enrico Tassi	check on baseuri	blob \| commitdiff \| raw \| diff to current
2005-07-06	Claudio Sacerdoti...	1. tactical "try_tacticals" renamed to "first"	blob \| commitdiff \| raw \| diff to current
2005-07-05	Ferruccio Guidi	name specifications added for elim_intros, elim_intros_...	blob \| commitdiff \| raw \| diff to current
2005-07-05	Enrico Tassi	now the moo contains also composed coercions (and It...	blob \| commitdiff \| raw \| diff to current
2005-07-05	Stefano Zacchiroli	ported to new getter interface	blob \| commitdiff \| raw \| diff to current
2005-07-04	Claudio Sacerdoti...	New command default "foo" uri1 ... urin	blob \| commitdiff \| raw \| diff to current
2005-07-04	Claudio Sacerdoti...	coercions are now stored in the .moo file.	blob \| commitdiff \| raw \| diff to current
2005-07-04	Claudio Sacerdoti...	Use eval_from_stream in place of eval_from_stream_ref...	blob \| commitdiff \| raw \| diff to current
2005-07-04	Claudio Sacerdoti...	"include" command implemented.	blob \| commitdiff \| raw \| diff to current
2005-07-04	Claudio Sacerdoti...	alias declarations are now put in the .moo file.	blob \| commitdiff \| raw \| diff to current
2005-07-01	Claudio Sacerdoti...	Signature of fwdSimpl changed to get rid of a warning.	blob \| commitdiff \| raw \| diff to current
2005-06-30	Claudio Sacerdoti...	Signature and concrete syntax of fold fixed.	blob \| commitdiff \| raw \| diff to current
2005-06-30	Ferruccio Guidi	lapply and fwd improved	blob \| commitdiff \| raw \| diff to current
2005-06-30	Claudio Sacerdoti...	1. rewrite_* and rewrite_back_* merged into one function	blob \| commitdiff \| raw \| diff to current
2005-06-30	Enrico Tassi	first matitadep snapshot	blob \| commitdiff \| raw \| diff to current
2005-06-29	Claudio Sacerdoti...	1. new syntax for patterns:	blob \| commitdiff \| raw \| diff to current
2005-06-29	Enrico Tassi	now baseuri is needed in each file (and its redefinitio...	blob \| commitdiff \| raw \| diff to current
2005-06-28	Enrico Tassi	* new binary matitatop	blob \| commitdiff \| raw \| diff to current
2005-06-28	Claudio Sacerdoti...	New argument for LApply: the ident for the generated...	blob \| commitdiff \| raw \| diff to current
2005-06-27	Claudio Sacerdoti...	replace generalized to patterns	blob \| commitdiff \| raw \| diff to current
2005-06-27	Claudio Sacerdoti...	A few other tactics made available to matita.	blob \| commitdiff \| raw \| diff to current
2005-06-27	Claudio Sacerdoti...	New argument (the identifier) to generalize.	blob \| commitdiff \| raw \| diff to current
2005-06-27	Claudio Sacerdoti...	New argument (the hypothesis name) for cut.	blob \| commitdiff \| raw \| diff to current
2005-06-27	Enrico Tassi	fized disambiguation of LApply	blob \| commitdiff \| raw \| diff to current
2005-06-27	Claudio Sacerdoti...	* the auto AST now has the width	blob \| commitdiff \| raw \| diff to current
2005-06-27	Claudio Sacerdoti...	* More tactics are now available to matita.	blob \| commitdiff \| raw \| diff to current
2005-06-25	Ferruccio Guidi	first working (?) version of lapply	blob \| commitdiff \| raw \| diff to current
2005-06-24	Ferruccio Guidi	lapply tactic continued	blob \| commitdiff \| raw \| diff to current
2005-06-24	Claudio Sacerdoti...	Asts generalized: a lot of tactics where restricted...	blob \| commitdiff \| raw \| diff to current
2005-06-23	Claudio Sacerdoti...	Tactic discriminate activated in matita.	blob \| commitdiff \| raw \| diff to current
2005-06-23	Claudio Sacerdoti...	1. Tactic generalize ported to patterns and activated...	blob \| commitdiff \| raw \| diff to current
2005-06-17	Enrico Tassi	support for goal patterns	blob \| commitdiff \| raw \| diff to current
2005-06-17	Claudio Sacerdoti...	more strings to UriManager.uri	blob \| commitdiff \| raw \| diff to current
2005-06-16	Stefano Zacchiroli	uses auto_tac_new instead of auto_tac	blob \| commitdiff \| raw \| diff to current
2005-06-16	Claudio Sacerdoti...	Dead code clean-up.	blob \| commitdiff \| raw \| diff to current
2005-06-15	Claudio Sacerdoti...	The `Record class now records also the name of the...	blob \| commitdiff \| raw \| diff to current
2005-06-15	Ferruccio Guidi	support for the new tactics lapply and fwd	blob \| commitdiff \| raw \| diff to current
2005-06-15	Claudio Sacerdoti...	Big commit and major code clean-up:	blob \| commitdiff \| raw \| diff to current
2005-06-13	Enrico Tassi	removed prerr_endline	blob \| commitdiff \| raw \| diff to current
2005-06-10	Enrico Tassi	added records	blob \| commitdiff \| raw \| diff to current
2005-06-10	Claudio Sacerdoti...	Got rid of a few bugs.	blob \| commitdiff \| raw \| diff to current
2005-06-09	Claudio Sacerdoti...	Error message improved.	blob \| commitdiff \| raw \| diff to current
2005-06-09	Enrico Tassi	added whd before uri_of_term	blob \| commitdiff \| raw \| diff to current
2005-06-08	Stefano Zacchiroli	rewritten cicBrowser handling of uri text entry, still...	blob \| commitdiff \| raw \| diff to current
2005-06-08	Claudio Sacerdoti...	More informative error message.	blob \| commitdiff \| raw \| diff to current
2005-06-07	Enrico Tassi	added letin	blob \| commitdiff \| raw \| diff to current
2005-06-01	Enrico Tassi	reduce with path	blob \| commitdiff \| raw \| diff to current
2005-06-01	Enrico Tassi	some cosmetic fixes	blob \| commitdiff \| raw \| diff to current
2005-05-31	Andrea Asperti	added automathic aliases for _ind _rec and _rect when...	blob \| commitdiff \| raw \| diff to current
2005-05-31	Enrico Tassi	added automathic aliases for qed and definition	blob \| commitdiff \| raw \| diff to current
2005-05-30	Andrea Asperti	added intros n.	blob \| commitdiff \| raw \| diff to current
2005-05-30	Andrea Asperti	added automathic aliases.	blob \| commitdiff \| raw \| diff to current
2005-05-27	Enrico Tassi	fixed matitac	blob \| commitdiff \| raw \| diff to current
2005-05-24	Enrico Tassi	added simpl	blob \| commitdiff \| raw \| diff to current
2005-05-24	Andrea Asperti	fix	blob \| commitdiff \| raw \| diff to current
2005-05-24	Andrea Asperti	elim -> elim_intros (no simpl)	blob \| commitdiff \| raw \| diff to current
2005-05-16	Enrico Tassi	added comments, fixed history, added loadList to browser	blob \| commitdiff \| raw \| diff to current
2005-05-02	Enrico Tassi	attached auto	blob \| commitdiff \| raw \| diff to current
2005-04-27	Stefano Zacchiroli	checked in new version of matita from svn	blob \| commitdiff \| raw \| diff to current

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

RSS Atom