]> matita.cs.unibo.it Git - helm.git/history - matita/matita/lib/basics
some notation renamed and fixed
[helm.git] / matita / matita / lib / basics /
2013-10-28 Andrea AspertiSplitted star
2013-10-02 Andrea Aspertia vector of finsets is a finset (in progress)
2013-09-07 Ferruccio Guidisupport for nat-labeled reflexive and transitive closur...
2013-08-09 Ferruccio Guidi- we added nat-labeled reflexive and transitive closure...
2013-08-01 Ferruccio Guidipartial commit: just the components before "static...
2013-06-05 Ferruccio Guidisome work on extended reduction ...
2013-05-17 Andrea AspertiImproved version
2013-05-17 Andrea Aspertimore functions
2013-04-29 Andrea AspertiA few integrations (closed an axiom in finset).
2013-04-25 Wilmer RicciottiAn attempt at ostensiby named syntax.
2013-02-07 Andrea AspertiA few integrations
2013-01-18 Ferruccio Guidi- paths and left residuals: second case of the equivale...
2013-01-18 Andrea Aspertihigh level semantics
2013-01-17 Andrea AspertiMoved a list comparison function in the list file
2013-01-16 Ferruccio Guidi- paths and left residuals: first case of the equivalen...
2013-01-15 Ferruccio Guidi- some additions and renaming ...
2013-01-02 Ferruccio Guidilambda: some refactoring + support for subsets of subte...
2012-12-28 Ferruccio Guidixoa: change in naming convenctions for existential...
2012-12-21 Andrea Aspertimem/append lemmas
2012-12-18 Ferruccio Guidi- star.ma: strip lemma and confluence of star
2012-12-17 Ferruccio Guidi- lambda: some parts commented out, some refactoring
2012-12-10 Ferruccio Guidi- lambda: - normalization theorem completed!
2012-12-09 Ferruccio Guidi- lambda: first half of the standardization theorem...
2012-12-08 Ferruccio Guidi- list.ma: improved notation for constant lists (a...
2012-12-07 Ferruccio Guidilstar removed from list.ma and placed in its own file
2012-12-06 Ferruccio Guidi- we enabled a notation for ex2
2012-12-01 Ferruccio Guidi- lambda: parallel reduction to obtain diamond property
2012-11-28 Ferruccio Guidi- relations.ma:
2012-11-15 Wilmer Ricciottisome more lemmata
2012-11-13 Wilmer Ricciottiprogress
2012-11-13 Andrea Aspertibasic lemmas
2012-11-12 Andrea Aspertiaddenda
2012-11-07 Ferruccio Guidi- predefined_virtuals: nwe characters
2012-10-27 Ferruccio Guidi- some additions and corrections
2012-10-18 Ferruccio Guidi- some confluence results for focalized reduction and...
2012-10-16 Ferruccio Guidicontext-free parallel reduction on closures is confluent!
2012-09-03 Ferruccio Guidilambda_delta: partial commit ...
2012-08-08 Wilmer RicciottiAdding GRealize to uni_step.
2012-07-23 Ferruccio Guidi- lambda_delta: we updated some notation
2012-06-20 Ferruccio Guidi- star.ma: constructor inj of star conflicts with previ...
2012-06-08 Andrea AspertiDropping a coercion and some hints due to conflicts...
2012-06-06 Andrea AspertiRestructuring
2012-06-05 Andrea AspertiSome results on relations. Moved things around.
2012-06-04 Andrea Aspertisemantics of the if-machine.
2012-06-01 Wilmer RicciottiFinalized copy sub-machine of the universal turing...
2012-05-28 Andrea Aspertimore typos
2012-05-28 Andrea Aspertitypos
2012-05-28 Andrea Aspertigraph of a function
2012-05-28 Andrea AspertiFinOpt
2012-05-28 Andrea Aspertimem, split
2012-05-25 Andrea AspertiNew definition of finset.
2012-05-17 Andrea Aspertifiltering on a list without repetitions
2012-05-16 Claudio Sacerdoti... Removed duplicated notation and interaction with the...
2012-05-16 Claudio Sacerdoti... Added alias instance=1 to avoid interaction with the...
2012-05-15 Claudio Sacerdoti... Patch by Ferruccio that enables \top/\bot for False...
2012-05-15 Ferruccio Guidiwe added the standard notation for True and False ...
2012-05-10 Ferruccio Guidi- lib: some additions
2012-05-07 Andrea Aspertistarl
2012-05-04 Claudio Sacerdoti... (no commit message)
2012-05-04 Claudio Sacerdoti... (no commit message)
2012-05-04 Wilmer RicciottiAdded a turing/universal directory for the universal...
2012-05-03 Andrea Aspertiprod fin set
2012-05-03 Andrea Aspertibool and segments of natural numbers
2012-04-27 Andrea AspertiExtensions to finset (sum) and auxiliary lemmas.
2012-04-26 Ferruccio Guidi- notation (possibly affecting all .ma files):
2012-04-04 Andrea AspertiAdded in basics
2012-03-23 Ferruccio Guidi- pts: we restored the former hierarchy
2012-03-19 Ferruccio Guidi- basics: bug fix in Conf3, it was not generic enough
2012-03-17 Ferruccio Guidi- basics: some support for abstract triangular confluen...
2012-03-15 Ferruccio Guidi- lambda_delta: strong normalization of simply typed...
2012-03-08 Andrea AspertiAxiom proved
2012-03-04 Ferruccio Guidi- lambda_delta: "conversion" and "equivalence" componen...
2012-01-31 Claudio Sacerdoti... Notation for destructuring let-in for triples fixed.
2012-01-03 Andrea Aspertimodified definition of memb
2012-01-03 Andrea Aspertireverse
2012-01-03 Andrea Aspertimore properties of union
2012-01-03 Andrea Aspertinoteq_to_eqnot
2011-12-15 Andrea AspertiSplitted DeqSets in their own file. Notation for memb...
2011-12-14 Claudio Sacerdoti... More stuff from CerCo to the standard library.
2011-12-14 Claudio Sacerdoti... Some more lemmas from CerCo.
2011-12-14 Claudio Sacerdoti... 1) Notation for dependent pairs differentiated from...
2011-12-13 Claudio Sacerdoti... Dependent pairs (i.e. Sigma types in Type[0]) are back...
2011-12-13 Claudio Sacerdoti... 1) PSig and Sig merged into a single Sigma type in...
2011-12-13 Claudio Sacerdoti... inject/eject replaced by mk_Sig/pi1.
2011-12-13 Claudio Sacerdoti... 1) New file russell with the coercions to activate...
2011-12-13 Andrea AspertiSig in Prop
2011-12-13 Claudio Sacerdoti... More stuff integrated from CerCo on sigma types (that...
2011-12-12 Claudio Sacerdoti... pair => mk_Prod (one more was left in notation)
2011-12-12 Claudio Sacerdoti... precedence level of if-then-else fixed
2011-12-12 Claudio Sacerdoti... Added elimination principles for destructuring let...
2011-12-12 Claudio Sacerdoti... Some integrations from CerCo. In particular:
2011-12-12 Claudio Sacerdoti... Pairs are now records.
2011-12-09 Andrea Aspertilist.ma moved inside lists.
2011-12-06 Ferruccio Guidiwe added a definition and a couple of lemmas
2011-12-06 Andrea AspertiListb contains some boolean functions over lists.
2011-12-06 Andrea Aspertinaive sets (A-> Prop)
2011-12-05 Andrea AspertiMore properties of iff
2011-11-21 Claudio Sacerdoti... {pattern} => in pattern;
2011-11-18 Claudio Sacerdoti... * Almost ready for release 0.99.1.
2011-11-16 Claudio Sacerdoti... Never ported to new syntax.
next