]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 146f8a5) | patch
1. All the reduction tactics have been modified to reduce several (sub)terms
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Jan 2003 13:20:55 +0000 (13:20 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Jan 2003 13:20:55 +0000 (13:20 +0000)
commitcf13b7adf17ce23342d8d5f26df6517aa222e21a
tree89492b10092494ea6f917e3c24294a5cbefc3a4btree | snapshot
parent146f8a58cd8c9aebe3d49df7f09e921f43c0c0e8commit | diff
1.  All the reduction tactics have been modified to reduce several (sub)terms
    at once.
2.  To reduce several (sub)terms at once you can use the new multiple
    selection feature.
helm/gTopLevel/gTopLevel.ml diff | blob | history
helm/gTopLevel/proofEngine.ml diff | blob | history
helm/gTopLevel/proofEngine.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.