Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-12-09 22:45:54 -0800 (Thu, 09 Dec 2004)
Revision: 6349
Log message:
with this commit [try]onAll[M][Cumulative]HypsT, onSomeHypT and
onAllMClausesOfAssumT skip contexts automatically.
As far as I understand this commit didn't affect any proofs.
It's possible that now some occurences of tryOnAll... can be replaced with
onAll...
Changes | Path |
+67 -12 | metaprl/tactics/proof/tacticals_boot.ml |