changeset 30729 | 461ee3e49ad3 |
parent 29614 | 1f7b1b0df292 |
child 31076 | 99fe356cbbc2 |
--- a/src/HOLCF/Bifinite.thy Thu Mar 26 19:24:21 2009 +0100 +++ b/src/HOLCF/Bifinite.thy Thu Mar 26 20:08:55 2009 +0100 @@ -37,7 +37,7 @@ by (rule finite_fixes_approx) qed -interpretation approx!: finite_deflation "approx i" +interpretation approx: finite_deflation "approx i" by (rule finite_deflation_approx) lemma (in deflation) deflation: "deflation d" ..