]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5b2c666) | patch
* Many improvements
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 18 Apr 2002 08:57:10 +0000 (08:57 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 18 Apr 2002 08:57:10 +0000 (08:57 +0000)
commitcbf6c7edd81459a9f22a5a8b5377b4f53297fd60
treec4de03a2698325d0fd25b352a34776fa30be9251tree | snapshot
parent5b2c666a48028daeba3fe6692e6ad3e14cad0a42commit | diff
* Many improvements
* The interface now gives the user the possibility of (re-)opening an existing
  constant.
* Tactic Elim no more exposed in the user interface. Replaced by ElimIntros.
* Selection of subterms in the hypothesis of the goal is now "sound".
* Reduction tactics (Whd, Reduce, Simpl) now work also on the hypothesis.
  New bug/feature: their changes are lost when moving to another goal
  and coming back afterwards.
helm/gTopLevel/gTopLevel.ml diff | blob | history
helm/gTopLevel/proofEngine.ml diff | blob | history
helm/gTopLevel/proofEngineReduction.ml diff | blob | history
helm/gTopLevel/sequentPp.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.