]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1416af9) | patch
1. Tactic generalize ported to patterns and activated in matita.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 23 Jun 2005 12:23:04 +0000 (12:23 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 23 Jun 2005 12:23:04 +0000 (12:23 +0000)
commite32693f30563379989b75b53c3be088396b732da
tree1c2134404bc88a8644408b3fa3191e07595af0a8tree | snapshot
parent1416af941615fa434b71c0adda461d5bcac65f89commit | diff
1. Tactic generalize ported to patterns and activated in matita.
2. slightly improved syntax for patterns
3. new test for "hand implemented" inversion (that uses induction instead of
   case analysis)
helm/matita/matita.lang diff | blob | history
helm/matita/matitaEngine.ml diff | blob | history
helm/matita/tests/inversion.ma [new file with mode: 0644] blob
helm/matita/tests/rewrite.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.