TY  - RPRT
TI  - The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
AU  - Lasse Blaauwbroek
AU  - Josef Urban
AU  - Herman Geuvers
PY  - 2020
DO  - 10.1007/978-3-030-53518-6_17
UR  - https://arxiv.org/abs/2008.00120
ID  - 2008.00120
ER  -