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