]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (from: cbf6c7e)
* 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)
* 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.


No differences found
Unnamed repository; edit this file 'description' to name the repository.