Re: [isabelle] Isar shortcut
Gabriele Pozzani wrote:
in many ML level demonstrations I seen that is possible to define a
containing a theorem list and so use it as simp's parameter.
val sels = [sbit_def, sq_def, ssending_def, rbit_def, rq_def,
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