Re: [isabelle] Isar shortcut

Gabriele Pozzani wrote:

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?

You could use

lemmas sels = sbit_def  sq_def  ssending_def  rbit_def  rq_def  rsending_def
show ?thesis by (simp add: sels)

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