equal
deleted
inserted
replaced
433 apply(regularize) |
433 apply(regularize) |
434 apply(rule impI) |
434 apply(rule impI) |
435 apply(simp) |
435 apply(simp) |
436 apply(rule allI) |
436 apply(rule allI) |
437 apply(rule list_eq_refl) |
437 apply(rule list_eq_refl) |
|
438 apply(cleaning) |
|
439 apply(simp add: fun_map.simps expand_fun_eq) |
|
440 apply(cleaning) |
438 done |
441 done |
439 |
442 |
440 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))" |
441 sorry |
444 sorry |
442 |
445 |
460 apply(subst babs_prs) |
463 apply(subst babs_prs) |
461 defer defer |
464 defer defer |
462 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
465 apply(tactic {* lambda_prs_tac @{context} 1 *}) |
463 (* Until here is ok *) |
466 (* Until here is ok *) |
464 apply(cleaning) |
467 apply(cleaning) |
|
468 sorry |
|
469 |
|
470 |
465 end |
471 end |