Constant ONE_SHOT_TACTICS 

pub const ONE_SHOT_TACTICS: &[(&str, &str)];

The closed one-shot tactic vocabulary of the literate Proof: surface: the keyword a mathematician writes, and the reflected tactic it applies to the reified goal. Adding a tactic is a row here — parse_proof_tactic and parse_single_tactic both read this table, so the two doors can never drift apart again.