]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e6a202a) | patch
- we added notation for the zetable and thetable items
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 21 Apr 2011 14:16:26 +0000 (14:16 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 21 Apr 2011 14:16:26 +0000 (14:16 +0000)
commit1df995bc8675c8b1118889cf470fc4d1d2ab5a22
tree0fbdb6e079d73488e74f85774b26083b7743de4ftree | snapshot
parente6a202ab70ee9f3f112616e41334576bc7561b74commit | diff
- we added notation for the zetable and thetable items
- the first inversion lemma for lift shows a bug in the destruct tactic :(
matita/matita/lib/lambda-delta/language/item.ma diff | blob | history
matita/matita/lib/lambda-delta/notation.ma diff | blob | history
matita/matita/lib/lambda-delta/substitution/lift.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.