diff -r f0aeca99b5d9 -r 461ee3e49ad3 src/HOLCF/Completion.thy --- a/src/HOLCF/Completion.thy Thu Mar 26 19:24:21 2009 +0100 +++ b/src/HOLCF/Completion.thy Thu Mar 26 20:08:55 2009 +0100 @@ -156,7 +156,7 @@ end -interpretation sq_le!: preorder "sq_le :: 'a::po \ 'a \ bool" +interpretation sq_le: preorder "sq_le :: 'a::po \ 'a \ bool" apply unfold_locales apply (rule refl_less) apply (erule (1) trans_less)