src/HOL/Basic_BNF_LFPs.thy

   unfolding xtor_def by (rule refl)
 
 lemmas xtor_inject = xtor_rel[of "op ="]
 
 lemma xtor_rel_induct: "(\<And>x y. vimage2p id_bnf id_bnf R x y \<Longrightarrow> IR (xtor x) (xtor y)) \<Longrightarrow> R \<le> IR"
-  unfolding xtor_def vimage2p_def id_bnf_def by default
+  unfolding xtor_def vimage2p_def id_bnf_def ..
 
 lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (id_bnf (Inl a)))"
   unfolding xtor_def id_bnf_def by (rule reflexive)
 
 lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (id_bnf (Inr a)))"

 
 lemma eq_snd_iff: "b = snd p \<longleftrightarrow> (\<exists>a. p = (a, b))"
   by (cases p) auto
 
 lemma ex_neg_all_pos: "((\<exists>x. P x) \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
-  by default blast+
+  by standard blast+
 
 lemma hypsubst_in_prems: "(\<And>x. y = x \<Longrightarrow> z = f x \<Longrightarrow> P) \<equiv> (z = f y \<Longrightarrow> P)"
-  by default blast+
+  by standard blast+
 
 lemma isl_map_sum:
   "isl (map_sum f g s) = isl s"
   by (cases s) simp_all