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

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

2007-10-16	Claudio Sacerdoti...	Interesting. Do we need many more inversion lemmas...	commit \| commitdiff \| tree
2007-10-16	Claudio Sacerdoti...	DOS-style CR+LF added to the blanks list.	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	Dead code clean-up.	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	The behaviour of autobatch paramodulation has changed.	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	Wrong test patched.	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	discriminate.ma => destruct.ma	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	Spurious code removed.	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	natural number => Coq natural number	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	Old wrong code to avoid old bug fixed.	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	Stupid bug fixed.	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	auto ==> autobatch	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	Stupid bug fixed (I deleted "assumption a" by error).	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	auto => autobatch	commit \| commitdiff \| tree
2007-10-15	Claudio Sacerdoti...	auto => autobatch	commit \| commitdiff \| tree
2007-10-14	Claudio Sacerdoti...	Caseness problems fixed.	commit \| commitdiff \| tree
2007-10-14	Claudio Sacerdoti...	Some lemmas moves to the file they belong to.	commit \| commitdiff \| tree
2007-10-12	Claudio Sacerdoti...	Move to OCaml 3.10. Requires debian packages from unstable...	commit \| commitdiff \| tree
2007-10-11	Claudio Sacerdoti...	Old inversion bug fixed: it used to work only on the...	commit \| commitdiff \| tree
2007-09-13	Claudio Sacerdoti...	added a debug print	commit \| commitdiff \| tree
2007-09-10	Claudio Sacerdoti...	This test shows one of the few cases were Matita is...	commit \| commitdiff \| tree
2007-09-05	Claudio Sacerdoti...	added fix case	commit \| commitdiff \| tree
2007-09-05	Claudio Sacerdoti...	coercions are propagated under Fix (but not mutually...	commit \| commitdiff \| tree
2007-09-04	Claudio Sacerdoti...	Dandling ")" removed from notation for 'exists.	commit \| commitdiff \| tree
2007-09-04	Claudio Sacerdoti...	Composition of coercions with arity > 0 is now implemented...	commit \| commitdiff \| tree
2007-09-04	Claudio Sacerdoti...	A test for propagation of coercions (that open new...	commit \| commitdiff \| tree
2007-09-04	Claudio Sacerdoti...	1. composition of coercions with saturations > 0 is...	commit \| commitdiff \| tree
2007-08-31	Claudio Sacerdoti...	alpha conversion to avoid case-insensitivity of MySql...	commit \| commitdiff \| tree
2007-08-31	Claudio Sacerdoti...	baseuri changed	commit \| commitdiff \| tree
2007-08-30	Claudio Sacerdoti...	Coercions are now generalized to the general form	commit \| commitdiff \| tree
2007-08-28	Claudio Sacerdoti...	* definition of implication free propositional formulas	commit \| commitdiff \| tree
2007-08-28	Claudio Sacerdoti...	A primer for Matita with some easy, medium, difficult...	commit \| commitdiff \| tree
2007-08-25	Claudio Sacerdoti...	thread-based interface activated again	commit \| commitdiff \| tree
2007-08-23	Claudio Sacerdoti...	Bug fixed: RewriteLR were not recognized correctly...	commit \| commitdiff \| tree
2007-08-23	Claudio Sacerdoti...	Bug fixed: the initial metasenv used in the two tactic...	commit \| commitdiff \| tree
2007-08-22	Claudio Sacerdoti...	Avoid reusing Hbeta several times.	commit \| commitdiff \| tree
2007-08-22	Claudio Sacerdoti...	select now works correctly even if multiple hypotheses...	commit \| commitdiff \| tree
2007-08-21	Claudio Sacerdoti...	Avoid confusion for names of proofs put in the applicative...	commit \| commitdiff \| tree
2007-08-21	Claudio Sacerdoti...	"obtain H E1=E2 by proof" is now working	commit \| commitdiff \| tree
2007-07-23	Claudio Sacerdoti...	Prototype of min_aux changed.	commit \| commitdiff \| tree
2007-07-20	Claudio Sacerdoti...	Another nicer version.	commit \| commitdiff \| tree
2007-07-20	Claudio Sacerdoti...	Even nicer script.	commit \| commitdiff \| tree
2007-07-20	Claudio Sacerdoti...	The nicest script obtained so far.	commit \| commitdiff \| tree
2007-07-20	Claudio Sacerdoti...	More simplification due to the new conversion strategy.	commit \| commitdiff \| tree
2007-07-20	Claudio Sacerdoti...	Script simplification due to the new efficient conversion...	commit \| commitdiff \| tree
2007-07-20	Claudio Sacerdoti...	Tentative bug fix for diverging pretty-printing function.	commit \| commitdiff \| tree
2007-07-20	Claudio Sacerdoti...	Initialization of matita.map_unicode_to_tex moved from...	commit \| commitdiff \| tree
2007-07-19	Claudio Sacerdoti...	Convertibility now converts machines in place of terms.	commit \| commitdiff \| tree
2007-07-19	Claudio Sacerdoti...	map_unicode_to_tex is no longer optional and it always...	commit \| commitdiff \| tree
2007-07-19	Claudio Sacerdoti...	paste_unicode_as_tex is now false by default; moreover...	commit \| commitdiff \| tree
2007-07-19	Claudio Sacerdoti...	Typo fixed.	commit \| commitdiff \| tree
2007-07-19	Claudio Sacerdoti...	Super-nice notation for the assembly stuff.	commit \| commitdiff \| tree
2007-07-17	Claudio Sacerdoti...	added missing parenthesis	commit \| commitdiff \| tree
2007-07-16	Claudio Sacerdoti...	More lemmas.	commit \| commitdiff \| tree
2007-07-16	Claudio Sacerdoti...	More daemons closed. A couple left in byte and many...	commit \| commitdiff \| tree
2007-07-16	Claudio Sacerdoti...	More daemons/axioms closed.	commit \| commitdiff \| tree
2007-07-16	Claudio Sacerdoti...	One daemon less.	commit \| commitdiff \| tree
2007-07-16	Claudio Sacerdoti...	More daemons got rid of (and more extra axioms to be...	commit \| commitdiff \| tree
2007-07-16	Claudio Sacerdoti...	Last daemon killed :-)	commit \| commitdiff \| tree
2007-07-16	Claudio Sacerdoti...	One less daemon (about "update"s).	commit \| commitdiff \| tree
2007-07-16	Claudio Sacerdoti...	All sub-proofs about "update" closed.	commit \| commitdiff \| tree
2007-07-16	Claudio Sacerdoti...	assembly.ma splitted into many files	commit \| commitdiff \| tree
2007-07-13	Claudio Sacerdoti...	More conjectures closed.	commit \| commitdiff \| tree
2007-07-13	Claudio Sacerdoti...	1. requires the new pretty printer for natural numbers	commit \| commitdiff \| tree
2007-07-13	Claudio Sacerdoti...	Dirty patch by Zack: natural numbers of Matita are...	commit \| commitdiff \| tree
2007-07-13	Claudio Sacerdoti...	Last crazy commit reverted.	commit \| commitdiff \| tree
2007-07-13	Claudio Sacerdoti...	Final theorem proved. Many many conjectures left. I...	commit \| commitdiff \| tree
2007-07-12	Claudio Sacerdoti...	The loop invariant I chosed was not correct!	commit \| commitdiff \| tree
2007-07-11	Claudio Sacerdoti...	Getting close to the final result.	commit \| commitdiff \| tree
2007-07-11	Claudio Sacerdoti...	1. loop invariant stated, but not proved	commit \| commitdiff \| tree
2007-07-11	Claudio Sacerdoti...	1. status factorized out in tick	commit \| commitdiff \| tree
2007-07-11	Claudio Sacerdoti...	auto new => autobatch	commit \| commitdiff \| tree
2007-07-11	Claudio Sacerdoti...	auto new => autobatch	commit \| commitdiff \| tree
2007-07-10	Claudio Sacerdoti...	0. less nice solution by Enrico reverted	commit \| commitdiff \| tree
2007-07-10	Claudio Sacerdoti...	New reduction strategy: the new reduction strategy...	commit \| commitdiff \| tree
2007-07-09	Claudio Sacerdoti...	Interesting theorem added (but still to be proved).	commit \| commitdiff \| tree
2007-07-05	Claudio Sacerdoti...	Exadecimal numbers are now used. This is a great speed-up.	commit \| commitdiff \| tree
2007-07-04	Claudio Sacerdoti...	Example program executed for x,y=0.	commit \| commitdiff \| tree
2007-07-04	Claudio Sacerdoti...	Quick hack: matita natural numbers are now accepted...	commit \| commitdiff \| tree
2007-07-04	Claudio Sacerdoti...	Bug fixed: a ~with_cast is now inserted when appropriate...	commit \| commitdiff \| tree
2007-07-04	Claudio Sacerdoti...	In place of conclude, obtain FIXMEXXX is now generated...	commit \| commitdiff \| tree
2007-07-04	Claudio Sacerdoti...	1. Code simplification	commit \| commitdiff \| tree
2007-07-04	Claudio Sacerdoti...	is_top_down was not propageted correctly under a bottom...	commit \| commitdiff \| tree
2007-07-04	Claudio Sacerdoti...	1. "by proof" now allowed as a justification in equality...	commit \| commitdiff \| tree
2007-07-04	Claudio Sacerdoti...	Added ~with_cast to the change tactic.	commit \| commitdiff \| tree
2007-07-04	Claudio Sacerdoti...	Bug fixed: name in letin was printed as "previous"...	commit \| commitdiff \| tree
2007-07-04	Claudio Sacerdoti...	More opcodes (badly) implemented.	commit \| commitdiff \| tree
2007-07-04	Claudio Sacerdoti...	List.ma: added function nth (with default value in...	commit \| commitdiff \| tree
2007-06-30	Claudio Sacerdoti...	In order to generate executable declarative scripts...	commit \| commitdiff \| tree
2007-06-30	Claudio Sacerdoti...	Bug fixed in bottom-up conversion.	commit \| commitdiff \| tree
2007-06-30	Claudio Sacerdoti...	BU Conversion was not generated for Rels fixed. I wonder...	commit \| commitdiff \| tree
2007-06-30	Claudio Sacerdoti...	Nicer layout but possibly more bugged.	commit \| commitdiff \| tree
2007-06-30	Claudio Sacerdoti...	Spurious "we need to prove" at the beginning of Intros...	commit \| commitdiff \| tree
2007-06-14	Claudio Sacerdoti...	Incompatible syntax problem between MySql e Sqlite3...	commit \| commitdiff \| tree
2007-06-04	Claudio Sacerdoti...	Another optimization, already done for geq.	commit \| commitdiff \| tree
2007-06-01	Claudio Sacerdoti...	Some interesting optimizations to prevent many bad...	commit \| commitdiff \| tree
2007-06-01	Claudio Sacerdoti...	Profiling enabled again.	commit \| commitdiff \| tree
next

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

RSS Atom