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