--- a/thys/MyInduction.thy	Fri Oct 10 18:45:10 2014 +0100
+++ b/thys/MyInduction.thy	Mon Oct 13 09:20:23 2014 +0100
@@ -1,3 +1,19 @@
 theory MyInduction
 imports Main
 begin
+
+fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"itrev [] ys = ys" |
+"itrev (x#xs) ys = itrev xs (x#ys)"
+
+lemma "itrev xs [] = rev xs"
+apply(induction xs)
+apply(auto)
+oops
+
+lemma "itrev xs ys = rev xs @ ys"
+apply(induction xs arbitrary: ys)
+apply auto
+done
+
+