4 

     5 fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where

     6 "itrev [] ys = ys" |

     7 "itrev (x#xs) ys = itrev xs (x#ys)"

     8 

     9 lemma "itrev xs [] = rev xs"

    10 apply(induction xs)

    11 apply(auto)

    12 oops

    13 

    14 lemma "itrev xs ys = rev xs @ ys"

    15 apply(induction xs arbitrary: ys)

    16 apply auto

    17 done

    18 

    19