mk_asm

bossLib.mk_asm : string -> thm -> tactic

Creates a new named assumption with the given name and the given fact.

Failure

Never fails.

See also

bossLib.asm, bossLib.asm_x