1signature blastLib = 2sig 3 val BBLAST_CONV : Conv.conv 4 val BBLAST_PROVE : Conv.conv 5 val BBLAST_PROVE_TAC : Tactic.tactic 6 val BBLAST_RULE : Conv.rule 7 val BBLAST_TAC : Tactic.tactic 8 val FULL_BBLAST_TAC : Tactic.tactic 9 val MP_BLASTABLE_TAC : Tactic.tactic 10end 11