src/HOLCF/Bifinite.thy
changeset 29237 e90d9d51106b
parent 28234 fc420a5cf72e
child 29252 ea97aa6aeba2
--- a/src/HOLCF/Bifinite.thy	Tue Dec 16 15:09:37 2008 +0100
+++ b/src/HOLCF/Bifinite.thy	Tue Dec 16 21:10:53 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Bifinite.thy
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
@@ -38,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" ..