[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?

Thanks
Gabriele Pozzani




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