503 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
503 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
504 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
504 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
505 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
505 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
506 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
506 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
507 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
507 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
508 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *}) |
508 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *}) |
509 apply assumption |
509 apply assumption |
510 apply (rule refl) |
510 apply (rule refl) |
511 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
511 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
512 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
512 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
513 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
513 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
514 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
514 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
515 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *}) |
515 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *}) |
516 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
516 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
517 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
517 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
518 apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *}) |
518 apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *}) |
519 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
519 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
520 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
520 apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *}) |
521 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *}) |
521 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *}) |
522 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
522 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
523 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
523 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
524 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
524 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
525 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
525 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
526 apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *}) |
526 apply (tactic {* clean_tac @{context} [quot] defs [(@{typ "('a list \<Rightarrow> 'c list \<Rightarrow> bool)"},@{typ "('a list \<Rightarrow> 'c fset \<Rightarrow> bool)"})] 1 *}) |