]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4e75ab4) | patch
- tdeq must imply tsts
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 13 Mar 2017 17:04:14 +0000 (17:04 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 13 Mar 2017 17:04:14 +0000 (17:04 +0000)
commit1de84a809c842fbc8a4e0d92b9bc61763c0e6fae
tree3bb5d6f140cd2a868f95aa1e6d8d3c54cf3f03c5tree | snapshot
parent4e75ab41fb7a0a9a4f66cb777a791ce3950c57cecommit | diff
- tdeq must imply tsts
- notational change for tsts
- refactoring
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/topiso_2.ma [deleted file] blob | history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/topiso_4.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/syntax/term_simple.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.ma diff | blob | history
matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_simple.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tdeq.ma [new file with mode: 0644] blob
matita/matita/contribs/lambdadelta/basic_2/syntax/tsts_tsts.ma diff | blob | history
matita/matita/predefined_virtuals.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.