[isabelle] Isar shortcut

Hello everybody,
in many ML level demonstrations I seen that is possible to define a variable
containing a theorem list and so use it as simp's parameter.

val sels = [sbit_def, sq_def, ssending_def, rbit_def, rq_def, rsending_def];
Goal ...
    by (asm_simp_tac (simpset() addsimps sels) 1);

Is there a way to do a same thing in Isar proofs?

Gabriele Pozzani

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.