equal
deleted
inserted
replaced
712 apply (rule Abs_fin_defl_mono) |
712 apply (rule Abs_fin_defl_mono) |
713 apply (rule finite_deflation_approx) |
713 apply (rule finite_deflation_approx) |
714 apply (rule finite_deflation_approx) |
714 apply (rule finite_deflation_approx) |
715 apply (rule chainE) |
715 apply (rule chainE) |
716 apply (rule chain_approx) |
716 apply (rule chain_approx) |
717 apply (simp add: cast_alg_defl_principal Abs_fin_defl_inverse finite_deflation_approx) |
717 apply (simp add: cast_alg_defl_principal |
|
718 Abs_fin_defl_inverse finite_deflation_approx) |
718 done |
719 done |
719 |
720 |
720 subsection {* Bifinite domains and algebraic deflations *} |
721 subsection {* Bifinite domains and algebraic deflations *} |
721 |
722 |
722 text {* This lemma says that if we have an ep-pair from |
723 text {* This lemma says that if we have an ep-pair from |