443   apply (rule b)

   443   apply (rule b)

   444   apply (assumption)

   444   apply (assumption)

   445   done

   445   done

   446 

   446 

   447 ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}

   447 ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}

   448 

   449 

   449 (* Construction site starts here *)

   450 (* Construction site starts here *)

   450 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"

   451 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"

   451 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})

   452 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})

   452 apply (tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})

   453 apply (tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})

   460 apply (rule IDENTITY_QUOTIENT)

   461 apply (rule IDENTITY_QUOTIENT)

   461 apply (rule IDENTITY_QUOTIENT)

   462 apply (rule IDENTITY_QUOTIENT)

   462 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})

   463 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})

   463 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})

   464 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})

   464 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})

   465 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})

   465 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})

   468 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})

   466 apply (rule IDENTITY_QUOTIENT)

   469 apply (rule IDENTITY_QUOTIENT)

   467 apply (rule IDENTITY_QUOTIENT)

   470 apply (rule IDENTITY_QUOTIENT)

   468 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})

   471 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})

   469 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})

   472 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *})