equal
deleted
inserted
replaced
479 apply clarify |
479 apply clarify |
480 apply (simp add: in_list_Suc_iff) |
480 apply (simp add: in_list_Suc_iff) |
481 apply clarify |
481 apply clarify |
482 apply (simp split: err.split_asm add: lem Err.sup_def lift2_def) |
482 apply (simp split: err.split_asm add: lem Err.sup_def lift2_def) |
483 apply (blast dest: lift2_eq_ErrD) |
483 apply (blast dest: lift2_eq_ErrD) |
484 apply blast |
|
485 done |
484 done |
486 |
485 |
487 lemma closed_err_lift2_conv: |
486 lemma closed_err_lift2_conv: |
488 "closed (err A) (lift2 f) = (!x:A. !y:A. x +_f y : err A)" |
487 "closed (err A) (lift2 f) = (!x:A. !y:A. x +_f y : err A)" |
489 apply (unfold closed_def) |
488 apply (unfold closed_def) |