equal
deleted
inserted
replaced
35 by (rule approx_less) |
35 by (rule approx_less) |
36 show "finite {x. approx i\<cdot>x = x}" |
36 show "finite {x. approx i\<cdot>x = x}" |
37 by (rule finite_fixes_approx) |
37 by (rule finite_fixes_approx) |
38 qed |
38 qed |
39 |
39 |
40 interpretation approx!: finite_deflation "approx i" |
40 interpretation approx: finite_deflation "approx i" |
41 by (rule finite_deflation_approx) |
41 by (rule finite_deflation_approx) |
42 |
42 |
43 lemma (in deflation) deflation: "deflation d" .. |
43 lemma (in deflation) deflation: "deflation d" .. |
44 |
44 |
45 lemma deflation_approx: "deflation (approx i)" |
45 lemma deflation_approx: "deflation (approx i)" |