101   and "\<And>pat1 pat2 c. \<lbrakk>\<And>c. P6 c pat1; \<And>c. P6 c pat2\<rbrakk> \<Longrightarrow> P6 c (PPair pat1 pat2)"

   101   and "\<And>pat1 pat2 c. \<lbrakk>\<And>c. P6 c pat1; \<And>c. P6 c pat2\<rbrakk> \<Longrightarrow> P6 c (PPair pat1 pat2)"

   102   shows "P1 c exp" and "P2 c fnclause" and "P3 c fnclauses" and "P4 c lrb" and "P5 c lrbs" and "P6 c pat"

   102   shows "P1 c exp" and "P2 c fnclause" and "P3 c fnclauses" and "P4 c lrb" and "P5 c lrbs" and "P6 c pat"

   103   apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *})

   103   apply(raw_tactic {* Induction_Schema.induction_schema_tac @{context} @{thms assms} *})

   104   apply(rule_tac y="exp" and c="c" in fun_recs.strong_exhaust(1))

   104   apply(rule_tac y="exp" and c="c" in fun_recs.strong_exhaust(1))

   105   apply(simp_all)[4]

   105   apply(simp_all)[4]

   107   apply(rule_tac ya="fnclause" and c="c" in fun_recs.strong_exhaust(2))

   106   apply(rule_tac ya="fnclause" and c="c" in fun_recs.strong_exhaust(2))

   108   apply(blast)

   107   apply(blast)

   109   apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3))

   108   apply(rule_tac yb="fnclauses" in fun_recs.strong_exhaust(3))

   110   apply(blast)

   109   apply(blast)

   111   apply(blast)

   110   apply(blast)