michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/run/tactic14): remove not_intro, it is not needed anymore

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-24 23:41:23 -07:00
parent 62483b793f
commit 905a1095f9
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/tactic14.lean
View file

@ -2,7 +2,7 @@ import standard
using tactic using tactic
definition basic_tac : tactic definition basic_tac : tactic
:= repeat [apply @and_intro | apply @not_intro | assumption] := repeat [apply @and_intro | assumption]
set_proof_qed basic_tac -- basic_tac is automatically applied to each element of a proof-qed block set_proof_qed basic_tac -- basic_tac is automatically applied to each element of a proof-qed block