-
Robbert Krebbers authored
The tactic "injection' H" now uses the name "H" for the first hypothesis it generates. Fresh names will still be used for the remaining hypotheses.
330702cc
The tactic "injection' H" now uses the name "H" for the first hypothesis it generates. Fresh names will still be used for the remaining hypotheses.