]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3ce1263) | patch
Inversion principles generation falls back to cases tactic when elim is not
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Mon, 23 Jan 2012 13:47:33 +0000 (13:47 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Mon, 23 Jan 2012 13:47:33 +0000 (13:47 +0000)
commite4328c9691fa85434acfb24eaedcb15ea2263b28
tree7fce0532ed9f7ee5a56541e81bc9867e660771c2tree | snapshot
parent3ce12633d55b42c4a5b4e3e601563747b873cc47commit | diff
Inversion principles generation falls back to cases tactic when elim is not
available.
matita/components/ng_tactics/nInversion.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.