[isabelle] effect of declare in Isar




I understand from the Isabelle/Isar conversion guide that

declare zless2p zle2p [simp] ;

should add these theorems to the current simpset, just like
the ML function call

Addsimps [zless2p, zle2p] ;

However it doesn't seem to work quite so, since in the following code

lemmas zless2p = zless2 [THEN zero_less_power] ;
lemmas zle2p = zless2p [THEN order_less_imp_le] ;
declare zless2p zle2p [simp] ;

ML {*
val zless2p = thm "zless2p" ;
val zle2p = thm "zle2p" ;
Addsimps [zless2p, zle2p] ;
*}

the ML section is necessary, since, without it, subsequent proofs in my theories don't work.

Can anyone tell me exactly what the Isar declare command does?

Thanks,

Jeremy





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