diff -r 16ffbc8442ca -r ffb5a181844b Nominal/Ex/Multi_Recs2.thy
--- a/Nominal/Ex/Multi_Recs2.thy	Sun Dec 26 16:35:16 2010 +0000
+++ b/Nominal/Ex/Multi_Recs2.thy	Tue Dec 28 00:20:50 2010 +0000
@@ -84,6 +84,44 @@
 thm fun_recs.supp
 
 
+
+
+lemma
+  fixes c::"'a::fs"
+  assumes "\<And>name c. P1 c (Var name)"
+  and "\<And>c. P1 c Unit"
+  and "\<And>exp1 exp2 c. \<lbrakk>\<And>c. P1 c exp1; \<And>c. P1 c exp2\<rbrakk> \<Longrightarrow> P1 c (Multi_Recs2.Pair exp1 exp2)"
+  and "\<And>lrbs exp c. \<lbrakk>b_lrbs lrbs \<sharp>* c; \<And>c. P5 c lrbs; \<And>c. P1 c exp\<rbrakk> \<Longrightarrow> P1 c (LetRec lrbs exp)"
+  and "\<And>name pat exp c. \<lbrakk>b_pat pat \<sharp>* c; \<And>c. P6 c pat; \<And>c. P1 c exp\<rbrakk> \<Longrightarrow> P2 c (K name pat exp)"
+  and "\<And>fnclause c. (\<And>c. P2 c fnclause) \<Longrightarrow> P3 c (S fnclause)"
+  and "\<And>fnclause fnclauses c. \<lbrakk>\<And>c. P2 c fnclause; \<And>c. P3 c fnclauses\<rbrakk> \<Longrightarrow> 
+    P3 c (ORs fnclause fnclauses)"
+  and "\<And>fnclauses c. (\<And>c. P3 c fnclauses) \<Longrightarrow> P4 c (Clause fnclauses)"
+  and "\<And>lrb c. (\<And>c. P4 c lrb) \<Longrightarrow> P5 c (Single lrb)"
+  and "\<And>lrb lrbs c. \<lbrakk>\<And>c. P4 c lrb; \<And>c. P5 c lrbs\<rbrakk> \<Longrightarrow> P5 c (More lrb lrbs)"
+  and "\<And>name c. P6 c (PVar name)"
+  and "\<And>c. P6 c PUnit"
+  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
+*}
+
+
 end