equal
deleted
inserted
replaced
462 using f3[simplified mem_def Respects_def] |
462 using f3[simplified mem_def Respects_def] |
463 apply(simp) |
463 apply(simp) |
464 apply(case_tac "a=b") |
464 apply(case_tac "a=b") |
465 apply(clarify) |
465 apply(clarify) |
466 apply(simp) |
466 apply(simp) |
467 apply(subst pt_swap_bij'') |
|
468 apply(rule pt_name_inst) |
|
469 apply(rule at_name_inst) |
|
470 apply(subst pt_swap_bij'') |
|
471 apply(rule pt_name_inst) |
|
472 apply(rule at_name_inst) |
|
473 apply(simp) |
|
474 apply(generate_fresh "name") |
|
475 (* probably true *) |
467 (* probably true *) |
476 sorry |
468 sorry |
477 |
469 |
478 lemma hom: |
470 lemma hom: |
479 "\<exists>hom\<in>Respects (alpha ===> op =). |
471 "\<exists>hom\<in>Respects (alpha ===> op =). |