equal
deleted
inserted
replaced
435 apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *}) |
435 apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *}) |
436 apply(tactic {* regularize_tac @{context} 1 *}) |
436 apply(tactic {* regularize_tac @{context} 1 *}) |
437 defer |
437 defer |
438 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
438 apply(tactic {* all_inj_repabs_tac @{context} 1*}) |
439 apply(tactic {* clean_tac @{context} 1 *}) |
439 apply(tactic {* clean_tac @{context} 1 *}) |
440 thm lambda_prs[OF identity_quotient Quotient_fset] |
440 apply(tactic {* clean_tac @{context} 1 *}) (* TODO: needs lambda_prs twice *) |
441 thm lambda_prs[OF identity_quotient Quotient_fset, simplified] |
|
442 apply(simp only: lambda_prs[OF identity_quotient Quotient_fset,simplified]) |
|
443 sorry |
441 sorry |
444 |
442 |
445 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))" |
443 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))" |
446 sorry |
444 sorry |
447 |
445 |