--- a/thys/MyInduction.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-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
-
-