diff -r ffb5a181844b -r 8268b277d240 Nominal/Ex/Multi_Recs2.thy
--- a/Nominal/Ex/Multi_Recs2.thy	Tue Dec 28 00:20:50 2010 +0000
+++ b/Nominal/Ex/Multi_Recs2.thy	Tue Dec 28 19:51:25 2010 +0000
@@ -104,23 +104,21 @@
   and "\<And>pat1 pat2 c. \<lbrakk>\<And>c. P6 c pat1; \<And>c. P6 c pat2\<rbrakk> \<Longrightarrow> P6 c (PPair pat1 pat2)"
   shows "P1 c exp" and "P2 c fnclause" and "P3 c fnclauses" and "P4 c lrb" and "P5 c lrbs" and "P6 c pat"
   apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *})
-oops
-
-ML {*
-  val trm1 = @{prop "P1 &&& P2 &&& P3"}
-  val trm2 = @{prop "(P1 &&& P2) &&& P3 &&& P4"}
-*}
-
-ML {*
-  Logic.dest_conjunction_list trm1;
-  Logic.dest_conjunction_list trm2
-*}
-
-ML {*
-  Logic.dest_conjunctions trm1;
-  Logic.dest_conjunctions trm2
-*}
-
+  apply(rule_tac y="exp" and c="c" in fun_recs.strong_exhaust(1))
+  apply(simp_all)[4]
+  apply(rule_tac ya="fnclause" and c="c" in fun_recs.strong_exhaust(2))
+  apply(simp_all)[1]
+  apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3))
+  apply(simp_all)[2]
+  apply(rule_tac yc="lrb" in fun_recs.strong_exhaust(4))
+  apply(simp_all)[1]
+  apply(rule_tac yd="lrbs" in fun_recs.strong_exhaust(5))
+  apply(simp_all)[2]
+  apply(rule_tac ye="pat" in fun_recs.strong_exhaust(6))
+  apply(simp_all)[3]
+  apply(tactic {* prove_termination_ind @{context} 1 *})
+  apply(simp_all add: fun_recs.size)
+  done
 
 end