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

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

2011-12-16	Andrea Asperti	In case paramodulation fails we apply unit equalities.	commit \| commitdiff \| tree
2011-12-15	Andrea Asperti	Splitted DeqSets in their own file. Notation for memb...	commit \| commitdiff \| tree
2011-12-15	Andrea Asperti	Hints sui DeqSets	commit \| commitdiff \| tree
2011-12-13	Andrea Asperti	Splitted re into lang.ma nd re.ma	commit \| commitdiff \| tree
2011-12-13	Andrea Asperti	Sig in Prop	commit \| commitdiff \| tree
2011-12-12	Andrea Asperti	Generalization to any alphabet. We do not need a finite	commit \| commitdiff \| tree
2011-12-09	Andrea Asperti	list.ma moved inside lists.	commit \| commitdiff \| tree
2011-12-09	Andrea Asperti	closing more axioms	commit \| commitdiff \| tree
2011-12-07	Andrea Asperti	Closing some axioms...	commit \| commitdiff \| tree
2011-12-07	Andrea Asperti	\vee notation for boolean or	commit \| commitdiff \| tree
2011-12-06	Andrea Asperti	Listb contains some boolean functions over lists.	commit \| commitdiff \| tree
2011-12-06	Andrea Asperti	naive sets (A-> Prop)	commit \| commitdiff \| tree
2011-12-05	Andrea Asperti	More properties of iff	commit \| commitdiff \| tree
2011-12-05	Andrea Asperti	Decidability of equality (draft)	commit \| commitdiff \| tree
2011-11-21	Andrea Asperti	regular expressions	commit \| commitdiff \| tree
2011-11-21	Andrea Asperti	Filtering all equations that cannot be embedded (containing...	commit \| commitdiff \| tree
2011-11-21	Andrea Asperti	Passing the correct subst a metasenv when idexing local...	commit \| commitdiff \| tree
2011-11-21	Andrea Asperti	Passing the right subst and metasenv when indexing...	commit \| commitdiff \| tree
2011-11-21	Andrea Asperti	Added a test for paramodulation filtering terms with...	commit \| commitdiff \| tree
2011-11-21	Andrea Asperti	More debugging info	commit \| commitdiff \| tree
2011-11-21	Andrea Asperti	Assert false removed (in line with the variable case).	commit \| commitdiff \| tree
2011-11-21	Andrea Asperti	Typo in comment	commit \| commitdiff \| tree
2011-11-16	Andrea Asperti	inversion replaced by elim (???)	commit \| commitdiff \| tree
2011-11-15	Andrea Asperti	non-facts local candidates must be applied too in presence of	commit \| commitdiff \| tree
2011-11-15	Andrea Asperti	non-facts local candidates must be applied too in presence of	commit \| commitdiff \| tree
2011-11-14	Andrea Asperti	Assert false is no longer true due to tooflex filtering.	commit \| commitdiff \| tree
2011-11-14	Andrea Asperti	Too flexible terms are pruned.	commit \| commitdiff \| tree
2011-11-07	Andrea Asperti	Removed some dead code.	commit \| commitdiff \| tree
2011-11-07	Andrea Asperti	New management of justifications.	commit \| commitdiff \| tree
2011-11-03	Andrea Asperti	1. we compare the expected branching with the actual...	commit \| commitdiff \| tree
2011-11-03	Andrea Asperti	At top level, we reindex the local equations for each...	commit \| commitdiff \| tree
2011-11-02	Andrea Asperti	The proof of append_cons used transitive_eq, not indexed.	commit \| commitdiff \| tree
2011-11-02	Andrea Asperti	Disabled printings.	commit \| commitdiff \| tree
2011-11-02	Andrea Asperti	--Tre the expected branching with the actual one and	commit \| commitdiff \| tree
2011-10-28	Andrea Asperti	New management of resulting subst in deep_eq: used...	commit \| commitdiff \| tree
2011-10-28	Andrea Asperti	-applicative_case has been rewritten and simplified;	commit \| commitdiff \| tree
2011-10-28	Andrea Asperti	Some qed-	commit \| commitdiff \| tree
2011-10-28	Andrea Asperti	some qed-	commit \| commitdiff \| tree
2011-10-28	Andrea Asperti	New management of the resulting substitution in deep eq.	commit \| commitdiff \| tree
2011-10-28	Andrea Asperti	-pplicative_case has been rewritten and simplified;	commit \| commitdiff \| tree
2011-10-21	Andrea Asperti	Now it should compile :-)	commit \| commitdiff \| tree
2011-10-21	Andrea Asperti	Optimization. Check removed.	commit \| commitdiff \| tree
2011-10-21	Andrea Asperti	Disabled debug.	commit \| commitdiff \| tree
2011-10-20	Andrea Asperti	1. ported to camlp5	commit \| commitdiff \| tree
2011-10-20	Andrea Asperti	typos	commit \| commitdiff \| tree
2011-10-20	Andrea Asperti	We order alternatives according to the number of subgoals...	commit \| commitdiff \| tree
2011-10-20	Andrea Asperti	QED takes a boolean parameter governing indexing.	commit \| commitdiff \| tree
2011-10-20	Andrea Asperti	Alternatives are ordered according to the number of...	commit \| commitdiff \| tree
2011-10-10	Andrea Asperti	Ported changes amde on the main branch:	commit \| commitdiff \| tree
2011-10-10	Andrea Asperti	- Reintroduction of a failure chache	commit \| commitdiff \| tree
2011-09-21	Andrea Asperti	Map in NCicUtils now takes an optional boolea to disable...	commit \| commitdiff \| tree
2011-09-20	Andrea Asperti	The Blob is not abstracted on the context any more.	commit \| commitdiff \| tree
2011-06-21	Andrea Asperti	Some progress	commit \| commitdiff \| tree
2011-06-20	Andrea Asperti	ported reduction.ma	commit \| commitdiff \| tree
2011-06-20	Andrea Asperti	Ported par_reduction	commit \| commitdiff \| tree
2011-06-20	Andrea Asperti	ported substs and subterms	commit \| commitdiff \| tree
2011-06-17	Andrea Asperti	New syntax of dummy with the type	commit \| commitdiff \| tree
2011-06-17	Andrea Asperti	Added a copy of lambdaN to extend the syntax of dummies...	commit \| commitdiff \| tree
2011-05-23	Andrea Asperti	Removed dead code	commit \| commitdiff \| tree
2011-05-20	Andrea Asperti	want_indent bug fixed	commit \| commitdiff \| tree
2011-05-20	Andrea Asperti	readded function box_of	commit \| commitdiff \| tree
2011-05-20	Andrea Asperti	Simplified rendering.	commit \| commitdiff \| tree
2011-05-20	Andrea Asperti	Simplified rendering	commit \| commitdiff \| tree
2011-05-20	Andrea Asperti	Simplified rendering	commit \| commitdiff \| tree
2011-05-20	Andrea Asperti	rm rendering attrs	commit \| commitdiff \| tree
2011-05-20	Andrea Asperti	Removed mathml and proof rendering.	commit \| commitdiff \| tree
2011-05-20	Andrea Asperti	Simplified rendering	commit \| commitdiff \| tree
2011-05-20	Andrea Asperti	Porting to new reduction.	commit \| commitdiff \| tree
2011-05-19	Andrea Asperti	Porting to the new pts.	commit \| commitdiff \| tree
2011-05-19	Andrea Asperti	Porting to new parametric TJ.	commit \| commitdiff \| tree
2011-05-19	Andrea Asperti	Dummies are blocked.	commit \| commitdiff \| tree
2011-05-18	Andrea Asperti	New version of TJ parametric in the specification of...	commit \| commitdiff \| tree
2011-05-11	Andrea Asperti	Partial modifications.	commit \| commitdiff \| tree
2011-04-20	Andrea Asperti	convertibility.	commit \| commitdiff \| tree
2011-04-20	Andrea Asperti	generatin lemmas and subject reduction (with a lot...	commit \| commitdiff \| tree
2011-04-20	Andrea Asperti	progress	commit \| commitdiff \| tree
2011-04-20	Andrea Asperti	error in the conversion rule	commit \| commitdiff \| tree
2011-03-23	Andrea Asperti	red star	commit \| commitdiff \| tree
2011-03-21	Andrea Asperti	sn_prod	commit \| commitdiff \| tree
2011-03-21	Andrea Asperti	sn_lambda	commit \| commitdiff \| tree
2011-03-21	Andrea Asperti	extensions	commit \| commitdiff \| tree
2011-03-11	Andrea Asperti	added star.ma (star closure of a relation)	commit \| commitdiff \| tree
2011-03-11	Andrea Asperti	Improvements.	commit \| commitdiff \| tree
2011-03-10	Andrea Asperti	diamond property	commit \| commitdiff \| tree
2011-03-07	Andrea Asperti	sottotermini e confluenza (manca pr_substs).	commit \| commitdiff \| tree
2011-02-10	Andrea Asperti	Added typing rule for dummies	commit \| commitdiff \| tree
2011-02-10	Andrea Asperti	Added lambda	commit \| commitdiff \| tree
2010-12-23	Andrea Asperti	Avoid duplicates in the list.	commit \| commitdiff \| tree
2010-12-23	Andrea Asperti	1. bug fixed: in the last commit on NCicLibrary we...	commit \| commitdiff \| tree
2010-12-23	Andrea Asperti	1. bug in addition of universe constraints fixed: the...	commit \| commitdiff \| tree
2010-12-23	Andrea Asperti	progress	commit \| commitdiff \| tree
2010-12-16	Andrea Asperti	New version of the library. Several files still do...	commit \| commitdiff \| tree
2010-12-16	Andrea Asperti	Some bugs fixed (and some still open) in recursive...	commit \| commitdiff \| tree
2010-12-16	Andrea Asperti	Bug fixed: a file A that includes a file B needs to...	commit \| commitdiff \| tree
2010-12-16	Andrea Asperti	Dead code removed.	commit \| commitdiff \| tree
2010-12-10	Andrea Asperti	Notation for - (clear).	commit \| commitdiff \| tree
2010-12-10	Andrea Asperti	Big change:	commit \| commitdiff \| tree
2010-12-10	Andrea Asperti	New syntax -H1 .. Hn for clear	commit \| commitdiff \| tree
2010-12-10	Andrea Asperti	Patch to avoid double creation of metavariables changed...	commit \| commitdiff \| tree
2010-12-06	Andrea Asperti	exp and factorial	commit \| commitdiff \| tree
next

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

RSS Atom