Function simp 

pub fn simp() -> Tactic

simp as a tactic value, its rule set drawn from everything in scope (premises, intro’d hypotheses, cited lemmas) — the script-level default.