]> matita.cs.unibo.it Git - helm.git/commit - helm/matita/tests/inversion.ma
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 059c1bb) | patch
New tactic: inversion.
authormarangon <??>
Thu, 15 Dec 2005 16:03:01 +0000 (16:03 +0000)
committermarangon <??>
Thu, 15 Dec 2005 16:03:01 +0000 (16:03 +0000)
commitde21be5819bd35a2cb83b3d33b1c578d970a32c7
tree8329c87596d25a9956e9e469374e7e78aef7118btree | snapshot
parent059c1bb4766e823aa53b39fed7d3dd55b4a06101commit | diff
New tactic: inversion.
 - only first phase implemented (no cleaning)
  - code in inversion.ml to be improved/cleaned up
helm/matita/tests/inversion.ma diff | blob | history
helm/matita/tests/inversion2.ma [new file with mode: 0644] blob
Unnamed repository; edit this file 'description' to name the repository.