--- a/src/HOL/Basic_BNF_LFPs.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Basic_BNF_LFPs.thy Sun Sep 13 22:56:52 2015 +0200
@@ -30,7 +30,7 @@
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)
@@ -60,10 +60,10 @@
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"