Re: [isabelle] simple proof over inductively defined relation (operational semantics)



>    lemma "2 : even"                                                            
Sorry, I had assumed you meant Suc(Suc 0). To convert a numeral like 2 into
Suc-form, use

apply(simp add:nat_number)

Tobias





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