]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cef076c) | patch
1. nInversion/nDestruct ported to work with jmeq properly
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 10 Oct 2011 13:52:59 +0000 (13:52 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 10 Oct 2011 13:52:59 +0000 (13:52 +0000)
commit8ea6d456f9e71babcf5adb2caee6ddd2b95047fb
tree78cb05f25f47b739ecb05e4e8b5c4ec1059b1ed9tree | snapshot
parentcef076c6fbd4ceec7c460414cf4421611457188dcommit | diff
1. nInversion/nDestruct ported to work with jmeq properly
2. axiom streicherK in logic.ma replaced with a computational proof
3. library changed accordingly
matita/components/ng_tactics/nDestructTac.ml diff | blob | history
matita/components/ng_tactics/nInversion.ml diff | blob | history
matita/components/ng_tactics/nnAuto.ml diff | blob | history
matita/matita/lib/basics/bool.ma diff | blob | history
matita/matita/lib/basics/jmeq.ma diff | blob | history
matita/matita/lib/basics/logic.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.