]> matita.cs.unibo.it Git - helm.git/history - matita/matita/lib/basics
match
[helm.git] / matita / matita / lib / basics /
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.
2011-11-16 Andrea Aspertiinversion replaced by elim (???)
2011-11-04 Ferruccio Guidi- lib: one lemma about equality was missing
2011-11-02 Claudio Sacerdoti... trans_eq and sym_eq indexing restored. Apparently they...
2011-11-02 Andrea AspertiThe proof of append_cons used transitive_eq, not indexed.
2011-10-28 Andrea Aspertisome qed-
2011-10-20 Wilmer RicciottiJMeq lifted to work on Type[1].
2011-10-10 Claudio Sacerdoti... 1. nInversion/nDestruct ported to work with jmeq properly
2011-06-21 Ferruccio Guidimissing ; to delimit syntax :(
2011-06-17 Claudio Sacerdoti... Remove the daemon :-)
2011-06-17 Andrea AspertiAdded a copy of lambdaN to extend the syntax of dummies...
2011-06-06 Claudio Sacerdoti... Minor changes because of the new, weaker (but much...
2011-05-30 Ferruccio Guidibasics: some additions
2011-04-28 Ferruccio Guidiwe uncommented R3 and R4 tu be used in lambda-delta
2011-03-21 Andrea Aspertiextensions
2011-03-11 Andrea Aspertiadded star.ma (star closure of a relation)
2011-03-09 Ferruccio Guidithe interpretation for Sigma was missing
2011-02-10 Andrea AspertiAdded lambda
2011-02-09 Wilmer Ricciottienabling destruct defs
2010-12-16 Andrea AspertiNew version of the library. Several files still do...