335 

   335 

   336 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"

   336 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"

   337 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})

   337 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})

   338 done

   338 done

   339 

   339 

   342 

   340 

   343 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"

   341 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"

   344 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})

   342 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})

   345 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})

   343 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})

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

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