--- a/thys/Rec_Def.thy	Fri Apr 05 09:18:17 2013 +0100
+++ b/thys/Rec_Def.thy	Mon Apr 22 08:26:16 2013 +0100
@@ -47,4 +47,16 @@
               \<forall> i < r. terminate f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs"
 
 
+inductive_cases terminate_pr_reverse: "terminate (Pr n f g) xs"
+
+inductive_cases terminate_z_reverse[elim!]: "terminate z xs"
+
+inductive_cases terminate_s_reverse[elim!]: "terminate s xs"
+
+inductive_cases terminate_id_reverse[elim!]: "terminate (id m n) xs"
+
+inductive_cases terminate_cn_reverse[elim!]: "terminate (Cn n f gs) xs"
+
+inductive_cases terminate_mn_reverse[elim!]:"terminate (Mn n f) xs"
+
 end
\ No newline at end of file