--- a/src/HOL/HOLCF/Bifinite.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Bifinite.thy Sun Sep 13 22:56:52 2015 +0200
@@ -162,7 +162,7 @@
qed
instance u :: (profinite) bifinite
- by default (rule profinite)
+ by standard (rule profinite)
text {*
Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
@@ -256,10 +256,10 @@
by (simp add: approx_chain_def cfun_eq_iff finite_deflation_bottom)
instance unit :: bifinite
- by default (fast intro!: approx_chain_unit)
+ by standard (fast intro!: approx_chain_unit)
instance discr :: (countable) profinite
- by default (fast intro!: discr_approx)
+ by standard (fast intro!: discr_approx)
instance lift :: (countable) bifinite
proof