]> matita.cs.unibo.it Git - helm.git/commit
* Many improvements
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 16 Apr 2002 11:14:07 +0000 (11:14 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 16 Apr 2002 11:14:07 +0000 (11:14 +0000)
commite627ae3edfbe950b87069b625ec9317acaf03ec5
treecd752406aae8bd3913cbc1056099c69070d7738b
parentc6a3408b6e603bed4f3d3c15f897b9007d98bb6f
* Many improvements
* Added the possibility to select parts of the goal of a sequent and retrieve
  the corresponding CIC term.
* New tactics implemented: Cut, Whd, Reduce, Simpl, Change
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/logicalOperations.ml
helm/gTopLevel/proofEngine.ml