theory Itrev = Main:

consts itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
primrec
"itrev [] ys = ys"
"itrev (x#xs) ys = itrev xs (x#ys)"

lemma "ALL ys. itrev xs ys = rev xs @ ys"
apply(induct_tac xs)
apply(auto)
done

end