--- a/src/Doc/Codegen/Adaptation.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/Doc/Codegen/Adaptation.thy Sun Sep 13 22:56:52 2015 +0200
@@ -346,7 +346,7 @@
definition %quote "HOL.equal (x::bar) y \<longleftrightarrow> x = y"
-instance %quote by default (simp add: equal_bar_def)
+instance %quote by standard (simp add: equal_bar_def)
end %quote (*<*)
--- a/src/HOL/Algebra/AbelCoset.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy Sun Sep 13 22:56:52 2015 +0200
@@ -236,7 +236,7 @@
by (rule a_normal)
show "abelian_subgroup H G"
- by default (simp add: a_comm)
+ by standard (simp add: a_comm)
qed
lemma abelian_subgroupI2:
--- a/src/HOL/Algebra/Divisibility.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Sun Sep 13 22:56:52 2015 +0200
@@ -25,14 +25,14 @@
and r_cancel:
"\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
shows "monoid_cancel G"
- by default fact+
+ by standard fact+
lemma (in monoid_cancel) is_monoid_cancel:
"monoid_cancel G"
..
sublocale group \<subseteq> monoid_cancel
- by default simp_all
+ by standard simp_all
locale comm_monoid_cancel = monoid_cancel + comm_monoid
@@ -3640,7 +3640,7 @@
done
sublocale factorial_monoid \<subseteq> primeness_condition_monoid
- by default (rule irreducible_is_prime)
+ by standard (rule irreducible_is_prime)
lemma (in factorial_monoid) primeness_condition:
@@ -3649,10 +3649,10 @@
lemma (in factorial_monoid) gcd_condition [simp]:
shows "gcd_condition_monoid G"
- by default (rule gcdof_exists)
+ by standard (rule gcdof_exists)
sublocale factorial_monoid \<subseteq> gcd_condition_monoid
- by default (rule gcdof_exists)
+ by standard (rule gcdof_exists)
lemma (in factorial_monoid) division_weak_lattice [simp]:
shows "weak_lattice (division_rel G)"
--- a/src/HOL/Algebra/Group.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Algebra/Group.thy Sun Sep 13 22:56:52 2015 +0200
@@ -286,7 +286,8 @@
qed
then have carrier_subset_Units: "carrier G <= Units G"
by (unfold Units_def) fast
- show ?thesis by default (auto simp: r_one m_assoc carrier_subset_Units)
+ show ?thesis
+ by standard (auto simp: r_one m_assoc carrier_subset_Units)
qed
lemma (in monoid) group_l_invI:
@@ -730,7 +731,7 @@
assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
x \<otimes> y = y \<otimes> x"
shows "comm_group G"
- by default (simp_all add: m_comm)
+ by standard (simp_all add: m_comm)
lemma comm_groupI:
fixes G (structure)
@@ -758,7 +759,7 @@
theorem (in group) subgroups_partial_order:
"partial_order \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
- by default simp_all
+ by standard simp_all
lemma (in group) subgroup_self:
"subgroup (carrier G) G"
--- a/src/HOL/Algebra/IntRing.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Algebra/IntRing.thy Sun Sep 13 22:56:52 2015 +0200
@@ -60,7 +60,7 @@
and "pow \<Z> x n = x^n"
proof -
-- "Specification"
- show "monoid \<Z>" by default auto
+ show "monoid \<Z>" by standard auto
then interpret int: monoid \<Z> .
-- "Carrier"
@@ -76,7 +76,7 @@
where "finprod \<Z> f A = setprod f A"
proof -
-- "Specification"
- show "comm_monoid \<Z>" by default auto
+ show "comm_monoid \<Z>" by standard auto
then interpret int: comm_monoid \<Z> .
-- "Operations"
@@ -94,7 +94,7 @@
and int_finsum_eq: "finsum \<Z> f A = setsum f A"
proof -
-- "Specification"
- show "abelian_monoid \<Z>" by default auto
+ show "abelian_monoid \<Z>" by standard auto
then interpret int: abelian_monoid \<Z> .
-- "Carrier"
@@ -178,7 +178,7 @@
and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
proof -
show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
- by default simp_all
+ by standard simp_all
show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
by simp
show "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
@@ -215,7 +215,7 @@
interpretation int (* [unfolded UNIV] *) :
total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
- by default clarsimp
+ by standard clarsimp
subsection {* Generated Ideals of @{text "\<Z>"} *}
--- a/src/HOL/Algebra/Lattice.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Algebra/Lattice.thy Sun Sep 13 22:56:52 2015 +0200
@@ -921,7 +921,7 @@
lemma (in weak_partial_order) weak_total_orderI:
assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
shows "weak_total_order L"
- by default (rule total)
+ by standard (rule total)
text {* Total orders are lattices. *}
@@ -985,7 +985,7 @@
and inf_exists:
"!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
shows "weak_complete_lattice L"
- by default (auto intro: sup_exists inf_exists)
+ by standard (auto intro: sup_exists inf_exists)
definition
top :: "_ => 'a" ("\<top>\<index>")
@@ -1133,14 +1133,14 @@
"[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
sublocale upper_semilattice < weak: weak_upper_semilattice
- by default (rule sup_of_two_exists)
+ by standard (rule sup_of_two_exists)
locale lower_semilattice = partial_order +
assumes inf_of_two_exists:
"[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
sublocale lower_semilattice < weak: weak_lower_semilattice
- by default (rule inf_of_two_exists)
+ by standard (rule inf_of_two_exists)
locale lattice = upper_semilattice + lower_semilattice
@@ -1191,19 +1191,19 @@
assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
sublocale total_order < weak: weak_total_order
- by default (rule total_order_total)
+ by standard (rule total_order_total)
text {* Introduction rule: the usual definition of total order *}
lemma (in partial_order) total_orderI:
assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
shows "total_order L"
- by default (rule total)
+ by standard (rule total)
text {* Total orders are lattices. *}
sublocale total_order < weak: lattice
- by default (auto intro: sup_of_two_exists inf_of_two_exists)
+ by standard (auto intro: sup_of_two_exists inf_of_two_exists)
text {* Complete lattices *}
@@ -1215,7 +1215,7 @@
"[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
sublocale complete_lattice < weak: weak_complete_lattice
- by default (auto intro: sup_exists inf_exists)
+ by standard (auto intro: sup_exists inf_exists)
text {* Introduction rule: the usual definition of complete lattice *}
@@ -1225,7 +1225,7 @@
and inf_exists:
"!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
shows "complete_lattice L"
- by default (auto intro: sup_exists inf_exists)
+ by standard (auto intro: sup_exists inf_exists)
theorem (in partial_order) complete_lattice_criterion1:
assumes top_exists: "EX g. greatest L g (carrier L)"
@@ -1282,7 +1282,7 @@
(is "complete_lattice ?L")
proof (rule partial_order.complete_latticeI)
show "partial_order ?L"
- by default auto
+ by standard auto
next
fix B
assume "B \<subseteq> carrier ?L"
--- a/src/HOL/Algebra/RingHom.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Algebra/RingHom.thy Sun Sep 13 22:56:52 2015 +0200
@@ -17,7 +17,7 @@
and hom_one [simp] = ring_hom_one [OF homh]
sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
- by default (rule homh)
+ by standard (rule homh)
sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
apply (rule abelian_group_homI)
--- a/src/HOL/Algebra/UnivPoly.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Sun Sep 13 22:56:52 2015 +0200
@@ -1760,7 +1760,7 @@
and deg_r_0: "deg R r = 0"
shows "r = monom P (eval R R id a f) 0"
proof -
- interpret UP_pre_univ_prop R R id P by default simp
+ interpret UP_pre_univ_prop R R id P by standard simp
have eval_ring_hom: "eval R R id a \<in> ring_hom P R"
using eval_ring_hom [OF a] by simp
have "eval R R id a f = eval R R id a ?gq \<oplus>\<^bsub>R\<^esub> eval R R id a r"
--- a/src/HOL/BNF_Fixpoint_Base.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/BNF_Fixpoint_Base.thy Sun Sep 13 22:56:52 2015 +0200
@@ -15,10 +15,10 @@
begin
lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
- by default simp_all
+ by standard simp_all
lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
- by default simp_all
+ by standard simp_all
lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
by auto
--- 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"
--- a/src/HOL/Complete_Partial_Order.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Complete_Partial_Order.thy Sun Sep 13 22:56:52 2015 +0200
@@ -293,7 +293,7 @@
end
instance complete_lattice \<subseteq> ccpo
- by default (fast intro: Sup_upper Sup_least)+
+ by standard (fast intro: Sup_upper Sup_least)+
lemma lfp_eq_fixp:
assumes f: "mono f" shows "lfp f = fixp f"
--- a/src/HOL/Conditionally_Complete_Lattices.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Sun Sep 13 22:56:52 2015 +0200
@@ -371,7 +371,7 @@
end
instance complete_lattice \<subseteq> conditionally_complete_lattice
- by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
+ by standard (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
lemma cSup_eq:
fixes a :: "'a :: {conditionally_complete_lattice, no_bot}"
--- a/src/HOL/Enum.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Enum.thy Sun Sep 13 22:56:52 2015 +0200
@@ -446,9 +446,10 @@
"enum_ex P = enum_ex (%x. enum_ex (%y. P (x, y)))"
-instance by default
- (simp_all add: enum_prod_def distinct_product
- enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def)
+instance
+ by standard
+ (simp_all add: enum_prod_def distinct_product
+ enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def)
end
--- a/src/HOL/Finite_Set.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Finite_Set.thy Sun Sep 13 22:56:52 2015 +0200
@@ -573,7 +573,7 @@
end
instance prod :: (finite, finite) finite
- by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
+ by standard (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
lemma inj_graph: "inj (%f. {(x, y). y = f x})"
by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
@@ -593,16 +593,16 @@
qed
instance bool :: finite
- by default (simp add: UNIV_bool)
+ by standard (simp add: UNIV_bool)
instance set :: (finite) finite
- by default (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)
+ by standard (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)
instance unit :: finite
- by default (simp add: UNIV_unit)
+ by standard (simp add: UNIV_unit)
instance sum :: (finite, finite) finite
- by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
+ by standard (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
subsection \<open>A basic fold functional for finite sets\<close>
@@ -967,7 +967,7 @@
"comp_fun_commute (\<lambda>x A'. if P x then Set.insert x A' else A')"
proof -
interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
- show ?thesis by default (auto simp: fun_eq_iff)
+ show ?thesis by standard (auto simp: fun_eq_iff)
qed
lemma Set_filter_fold:
@@ -988,7 +988,7 @@
shows "image f A = fold (\<lambda>k A. Set.insert (f k) A) {} A"
using assms
proof -
- interpret comp_fun_commute "\<lambda>k A. Set.insert (f k) A" by default auto
+ interpret comp_fun_commute "\<lambda>k A. Set.insert (f k) A" by standard auto
show ?thesis using assms by (induct A) auto
qed
@@ -997,7 +997,7 @@
shows "Ball A P = fold (\<lambda>k s. s \<and> P k) True A"
using assms
proof -
- interpret comp_fun_commute "\<lambda>k s. s \<and> P k" by default auto
+ interpret comp_fun_commute "\<lambda>k s. s \<and> P k" by standard auto
show ?thesis using assms by (induct A) auto
qed
@@ -1006,7 +1006,7 @@
shows "Bex A P = fold (\<lambda>k s. s \<or> P k) False A"
using assms
proof -
- interpret comp_fun_commute "\<lambda>k s. s \<or> P k" by default auto
+ interpret comp_fun_commute "\<lambda>k s. s \<or> P k" by standard auto
show ?thesis using assms by (induct A) auto
qed
@@ -1027,14 +1027,14 @@
assumes "finite B"
shows "(\<Union>y\<in>B. {(x, y)}) \<union> A = fold (\<lambda>y. Set.insert (x, y)) A B"
proof -
- interpret comp_fun_commute "\<lambda>y. Set.insert (x, y)" by default auto
+ interpret comp_fun_commute "\<lambda>y. Set.insert (x, y)" by standard auto
show ?thesis using assms by (induct B arbitrary: A) simp_all
qed
lemma comp_fun_commute_product_fold:
assumes "finite B"
shows "comp_fun_commute (\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B)"
-by default (auto simp: fold_union_pair[symmetric] assms)
+ by standard (auto simp: fold_union_pair[symmetric] assms)
lemma product_fold:
assumes "finite A"
@@ -1122,18 +1122,16 @@
begin
interpretation fold?: comp_fun_commute f
- by default (insert comp_fun_commute, simp add: fun_eq_iff)
+ by standard (insert comp_fun_commute, simp add: fun_eq_iff)
definition F :: "'a set \<Rightarrow> 'b"
where
eq_fold: "F A = fold f z A"
-lemma empty [simp]:
- "F {} = z"
+lemma empty [simp]:"F {} = z"
by (simp add: eq_fold)
-lemma infinite [simp]:
- "\<not> finite A \<Longrightarrow> F A = z"
+lemma infinite [simp]: "\<not> finite A \<Longrightarrow> F A = z"
by (simp add: eq_fold)
lemma insert [simp]:
@@ -1172,7 +1170,7 @@
declare insert [simp del]
interpretation fold?: comp_fun_idem f
- by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
+ by standard (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
lemma insert_idem [simp]:
assumes "finite A"
@@ -1202,7 +1200,7 @@
where
"folding.F (\<lambda>_. Suc) 0 = card"
proof -
- show "folding (\<lambda>_. Suc)" by default rule
+ show "folding (\<lambda>_. Suc)" by standard rule
then interpret card!: folding "\<lambda>_. Suc" 0 .
from card_def show "folding.F (\<lambda>_. Suc) 0 = card" by rule
qed
--- a/src/HOL/GCD.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/GCD.thy Sun Sep 13 22:56:52 2015 +0200
@@ -1975,7 +1975,7 @@
and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
proof -
show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
- by default (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
+ by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
then interpret gcd_lcm_complete_lattice_nat:
complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" .
--- a/src/HOL/Groups.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Groups.thy Sun Sep 13 22:56:52 2015 +0200
@@ -71,7 +71,7 @@
begin
sublocale monoid
- by default (simp_all add: commute comm_neutral)
+ by standard (simp_all add: commute comm_neutral)
end
@@ -132,7 +132,7 @@
begin
sublocale add!: semigroup plus
- by default (fact add_assoc)
+ by standard (fact add_assoc)
end
@@ -143,7 +143,7 @@
begin
sublocale add!: abel_semigroup plus
- by default (fact add_commute)
+ by standard (fact add_commute)
declare add.left_commute [algebra_simps, field_simps]
@@ -160,7 +160,7 @@
begin
sublocale mult!: semigroup times
- by default (fact mult_assoc)
+ by standard (fact mult_assoc)
end
@@ -171,7 +171,7 @@
begin
sublocale mult!: abel_semigroup times
- by default (fact mult_commute)
+ by standard (fact mult_commute)
declare mult.left_commute [algebra_simps, field_simps]
@@ -189,7 +189,7 @@
begin
sublocale add!: monoid plus 0
- by default (fact add_0_left add_0_right)+
+ by standard (fact add_0_left add_0_right)+
end
@@ -201,10 +201,10 @@
begin
subclass monoid_add
- by default (simp_all add: add_0 add.commute [of _ 0])
+ by standard (simp_all add: add_0 add.commute [of _ 0])
sublocale add!: comm_monoid plus 0
- by default (simp add: ac_simps)
+ by standard (simp add: ac_simps)
end
@@ -214,7 +214,7 @@
begin
sublocale mult!: monoid times 1
- by default (fact mult_1_left mult_1_right)+
+ by standard (fact mult_1_left mult_1_right)+
end
@@ -226,10 +226,10 @@
begin
subclass monoid_mult
- by default (simp_all add: mult_1 mult.commute [of _ 1])
+ by standard (simp_all add: mult_1 mult.commute [of _ 1])
sublocale mult!: comm_monoid times 1
- by default (simp add: ac_simps)
+ by standard (simp add: ac_simps)
end
--- a/src/HOL/Groups_Big.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Groups_Big.thy Sun Sep 13 22:56:52 2015 +0200
@@ -18,7 +18,7 @@
begin
interpretation comp_fun_commute f
- by default (simp add: fun_eq_iff left_commute)
+ by standard (simp add: fun_eq_iff left_commute)
interpretation comp?: comp_fun_commute "f \<circ> g"
by (fact comp_comp_fun_commute)
--- a/src/HOL/HOL.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOL.thy Sun Sep 13 22:56:52 2015 +0200
@@ -1254,10 +1254,10 @@
qed
lemma implies_True_equals: "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True"
-by default (intro TrueI)
+ by standard (intro TrueI)
lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
-by default simp_all
+ by standard simp_all
(* This is not made a simp rule because it does not improve any proofs
but slows some AFP entries down by 5% (cpu time). May 2015 *)
--- 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
--- a/src/HOL/HOLCF/Completion.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Completion.thy Sun Sep 13 22:56:52 2015 +0200
@@ -116,7 +116,7 @@
assumes type: "type_definition Rep Abs {S. ideal S}"
assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
shows "OFCLASS('b, cpo_class)"
-by (default, rule exI, erule typedef_ideal_lub [OF type below])
+ by standard (rule exI, erule typedef_ideal_lub [OF type below])
end
--- a/src/HOL/HOLCF/ConvexPD.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/ConvexPD.thy Sun Sep 13 22:56:52 2015 +0200
@@ -414,14 +414,14 @@
by (simp add: convex_map_def convex_bind_bind)
lemma ep_pair_convex_map: "ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)"
-apply default
+apply standard
apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse)
apply (induct_tac y rule: convex_pd_induct)
apply (simp_all add: ep_pair.e_p_below monofun_cfun)
done
lemma deflation_convex_map: "deflation d \<Longrightarrow> deflation (convex_map\<cdot>d)"
-apply default
+apply standard
apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem)
apply (induct_tac x rule: convex_pd_induct)
apply (simp_all add: deflation.below monofun_cfun)
--- a/src/HOL/HOLCF/Deflation.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Deflation.thy Sun Sep 13 22:56:52 2015 +0200
@@ -161,7 +161,7 @@
unfolding finite_deflation_def by simp
lemma finite_deflation_bottom: "finite_deflation \<bottom>"
-by default simp_all
+by standard simp_all
subsection {* Continuous embedding-projection pairs *}
@@ -358,7 +358,7 @@
subsection {* Composing ep-pairs *}
lemma ep_pair_ID_ID: "ep_pair ID ID"
-by default simp_all
+by standard simp_all
lemma ep_pair_comp:
assumes "ep_pair e1 p1" and "ep_pair e2 p2"
--- a/src/HOL/HOLCF/Discrete.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Discrete.thy Sun Sep 13 22:56:52 2015 +0200
@@ -19,7 +19,7 @@
"(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
instance
-by default (simp add: below_discr_def)
+ by standard (simp add: below_discr_def)
end
--- a/src/HOL/HOLCF/Domain.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Domain.thy Sun Sep 13 22:56:52 2015 +0200
@@ -125,7 +125,7 @@
unfolding prj_beta emb_beta
by (simp add: type_definition.Abs_inverse [OF type])
show "ep_pair (emb :: 'a \<rightarrow> udom) prj"
- apply default
+ apply standard
apply (simp add: prj_emb)
apply (simp add: emb_prj cast.below)
done
--- a/src/HOL/HOLCF/Fun_Cpo.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Fun_Cpo.thy Sun Sep 13 22:56:52 2015 +0200
@@ -93,7 +93,7 @@
by (simp add: below_fun_def)
instance "fun" :: (type, pcpo) pcpo
-by default (fast intro: minimal_fun)
+by standard (fast intro: minimal_fun)
lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
by (rule minimal_fun [THEN bottomI, symmetric])
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sun Sep 13 22:56:52 2015 +0200
@@ -490,7 +490,7 @@
by (fast intro: below_antisym meet_defl_below2 meet_defl_greatest)
interpretation meet_defl: semilattice "\<lambda>a b. meet_defl\<cdot>a\<cdot>b"
-by default
+by standard
(fast intro: below_antisym meet_defl_greatest
meet_defl_below1 [THEN below_trans] meet_defl_below2 [THEN below_trans])+
--- a/src/HOL/HOLCF/Library/List_Predomain.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Library/List_Predomain.thy Sun Sep 13 22:56:52 2015 +0200
@@ -143,7 +143,7 @@
lemma deflation_list_map [domain_deflation]:
"deflation d \<Longrightarrow> deflation (list_map d)"
-apply default
+apply standard
apply (induct_tac x, simp_all add: deflation.idem)
apply (induct_tac x, simp_all add: deflation.below)
done
--- a/src/HOL/HOLCF/Library/Option_Cpo.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy Sun Sep 13 22:56:52 2015 +0200
@@ -269,7 +269,7 @@
lemma deflation_option_map [domain_deflation]:
"deflation d \<Longrightarrow> deflation (option_map d)"
-apply default
+apply standard
apply (induct_tac x, simp_all add: deflation.idem)
apply (induct_tac x, simp_all add: deflation.below)
done
--- a/src/HOL/HOLCF/Library/Sum_Cpo.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy Sun Sep 13 22:56:52 2015 +0200
@@ -342,7 +342,7 @@
lemma deflation_map_sum [domain_deflation]:
"\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (map_sum' d1 d2)"
-apply default
+apply standard
apply (induct_tac x, simp_all add: deflation.idem)
apply (induct_tac x, simp_all add: deflation.below)
done
--- a/src/HOL/HOLCF/LowerPD.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/LowerPD.thy Sun Sep 13 22:56:52 2015 +0200
@@ -407,14 +407,14 @@
by (simp add: lower_map_def lower_bind_bind)
lemma ep_pair_lower_map: "ep_pair e p \<Longrightarrow> ep_pair (lower_map\<cdot>e) (lower_map\<cdot>p)"
-apply default
+apply standard
apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse)
apply (induct_tac y rule: lower_pd_induct)
apply (simp_all add: ep_pair.e_p_below monofun_cfun del: lower_plus_below_iff)
done
lemma deflation_lower_map: "deflation d \<Longrightarrow> deflation (lower_map\<cdot>d)"
-apply default
+apply standard
apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem)
apply (induct_tac x rule: lower_pd_induct)
apply (simp_all add: deflation.below monofun_cfun del: lower_plus_below_iff)
--- a/src/HOL/HOLCF/Map_Functions.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Map_Functions.thy Sun Sep 13 22:56:52 2015 +0200
@@ -195,13 +195,13 @@
by (simp add: cfcomp1 u_map_map eta_cfun)
lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
-apply default
+apply standard
apply (case_tac x, simp, simp add: ep_pair.e_inverse)
apply (case_tac y, simp, simp add: ep_pair.e_p_below)
done
lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
-apply default
+apply standard
apply (case_tac x, simp, simp add: deflation.idem)
apply (case_tac x, simp, simp add: deflation.below)
done
--- a/src/HOL/HOLCF/Pcpo.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Pcpo.thy Sun Sep 13 22:56:52 2015 +0200
@@ -198,7 +198,7 @@
begin
subclass cpo
-apply default
+apply standard
apply (frule chfin)
apply (blast intro: lub_finch1)
done
@@ -213,7 +213,7 @@
begin
subclass chfin
-apply default
+apply standard
apply (unfold max_in_chain_def)
apply (case_tac "\<forall>i. Y i = \<bottom>")
apply simp
--- a/src/HOL/HOLCF/Representable.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Representable.thy Sun Sep 13 22:56:52 2015 +0200
@@ -119,10 +119,10 @@
qed
instance "domain" \<subseteq> bifinite
-by default (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL])
+by standard (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL])
instance predomain \<subseteq> profinite
-by default (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
+by standard (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
subsection {* Universal domain ep-pairs *}
--- a/src/HOL/HOLCF/Universal.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Universal.thy Sun Sep 13 22:56:52 2015 +0200
@@ -98,7 +98,7 @@
done
interpretation udom: preorder ubasis_le
-apply default
+apply standard
apply (rule ubasis_le_refl)
apply (erule (1) ubasis_le_trans)
done
@@ -879,7 +879,7 @@
done
lemma ep_pair_udom: "ep_pair udom_emb udom_prj"
- apply default
+ apply standard
apply (rule compact_basis.principal_induct, simp)
apply (simp add: udom_emb_principal udom_prj_principal)
apply (simp add: basis_prj_basis_emb)
@@ -986,7 +986,7 @@
qed
instance udom :: bifinite
- by default (fast intro: udom_approx)
+ by standard (fast intro: udom_approx)
hide_const (open) node
--- a/src/HOL/HOLCF/UpperPD.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/UpperPD.thy Sun Sep 13 22:56:52 2015 +0200
@@ -400,14 +400,14 @@
by (simp add: upper_map_def upper_bind_bind)
lemma ep_pair_upper_map: "ep_pair e p \<Longrightarrow> ep_pair (upper_map\<cdot>e) (upper_map\<cdot>p)"
-apply default
+apply standard
apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse)
apply (induct_tac y rule: upper_pd_induct)
apply (simp_all add: ep_pair.e_p_below monofun_cfun del: upper_below_plus_iff)
done
lemma deflation_upper_map: "deflation d \<Longrightarrow> deflation (upper_map\<cdot>d)"
-apply default
+apply standard
apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem)
apply (induct_tac x rule: upper_pd_induct)
apply (simp_all add: deflation.below monofun_cfun del: upper_below_plus_iff)
--- a/src/HOL/Int.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Int.thy Sun Sep 13 22:56:52 2015 +0200
@@ -66,7 +66,7 @@
qed
instance
- by default (transfer, clarsimp simp: algebra_simps)+
+ by standard (transfer, clarsimp simp: algebra_simps)+
end
@@ -99,7 +99,7 @@
by auto
instance
- by default (transfer, force)+
+ by standard (transfer, force)+
end
@@ -305,13 +305,13 @@
instance int :: no_top
- apply default
+ apply standard
apply (rule_tac x="x + 1" in exI)
apply simp
done
instance int :: no_bot
- apply default
+ apply standard
apply (rule_tac x="x - 1" in exI)
apply simp
done
@@ -1526,7 +1526,8 @@
definition
"HOL.equal k l \<longleftrightarrow> k = (l::int)"
-instance by default (rule equal_int_def)
+instance
+ by standard (rule equal_int_def)
end
--- a/src/HOL/Lattices.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Lattices.thy Sun Sep 13 22:56:52 2015 +0200
@@ -145,7 +145,7 @@
begin
sublocale ordering_top less_eq less 1
- by default (simp add: order_iff)
+ by standard (simp add: order_iff)
end
@@ -283,7 +283,7 @@
qed
sublocale inf!: semilattice_order inf less_eq less
- by default (auto simp add: le_iff_inf less_le)
+ by standard (auto simp add: le_iff_inf less_le)
lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
by (fact inf.assoc)
@@ -328,7 +328,7 @@
qed
sublocale sup!: semilattice_order sup greater_eq greater
- by default (auto simp add: le_iff_sup sup.commute less_le)
+ by standard (auto simp add: le_iff_sup sup.commute less_le)
lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
by (fact sup.assoc)
@@ -717,7 +717,7 @@
sublocale min!: semilattice_order min less_eq less
+ max!: semilattice_order max greater_eq greater
- by default (auto simp add: min_def max_def)
+ by standard (auto simp add: min_def max_def)
lemma min_le_iff_disj:
"min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
--- a/src/HOL/Lattices_Big.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Lattices_Big.thy Sun Sep 13 22:56:52 2015 +0200
@@ -21,7 +21,7 @@
begin
interpretation comp_fun_idem f
- by default (simp_all add: fun_eq_iff left_commute)
+ by standard (simp_all add: fun_eq_iff left_commute)
definition F :: "'a set \<Rightarrow> 'a"
where
@@ -33,7 +33,7 @@
proof (rule sym)
let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
interpret comp_fun_idem "?f"
- by default (simp_all add: fun_eq_iff commute left_commute split: option.split)
+ by standard (simp_all add: fun_eq_iff commute left_commute split: option.split)
from assms show "Finite_Set.fold f x A = F (insert x A)"
proof induct
case empty then show ?case by (simp add: eq_fold')
@@ -189,7 +189,7 @@
begin
interpretation comp_fun_idem f
- by default (simp_all add: fun_eq_iff left_commute)
+ by standard (simp_all add: fun_eq_iff left_commute)
definition F :: "'a set \<Rightarrow> 'a"
where
@@ -496,9 +496,9 @@
"semilattice_set.F min = Min"
and "semilattice_set.F max = Max"
proof -
- show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
+ show "semilattice_order_set min less_eq less" by standard (auto simp add: min_def)
then interpret Min!: semilattice_order_set min less_eq less .
- show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
+ show "semilattice_order_set max greater_eq greater" by standard (auto simp add: max_def)
then interpret Max!: semilattice_order_set max greater_eq greater .
from Min_def show "semilattice_set.F min = Min" by rule
from Max_def show "semilattice_set.F max = Max" by rule
--- a/src/HOL/Limits.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Limits.thy Sun Sep 13 22:56:52 2015 +0200
@@ -710,13 +710,15 @@
lemma (in bounded_bilinear) flip:
"bounded_bilinear (\<lambda>x y. y ** x)"
- apply default
+ apply standard
apply (rule add_right)
apply (rule add_left)
apply (rule scaleR_right)
apply (rule scaleR_left)
apply (subst mult.commute)
- using bounded by fast
+ using bounded
+ apply fast
+ done
lemma (in bounded_bilinear) Bfun_prod_Zfun:
assumes f: "Bfun f F"
--- a/src/HOL/List.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/List.thy Sun Sep 13 22:56:52 2015 +0200
@@ -2868,7 +2868,7 @@
"F (set (x # xs)) = fold f xs x"
proof -
interpret comp_fun_idem f
- by default (simp_all add: fun_eq_iff left_commute)
+ by standard (simp_all add: fun_eq_iff left_commute)
show ?thesis by (simp add: eq_fold fold_set_fold)
qed
@@ -5161,7 +5161,7 @@
"folding.F insort [] = sorted_list_of_set"
proof -
interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
- show "folding insort" by default (fact comp_fun_commute)
+ show "folding insort" by standard (fact comp_fun_commute)
show "folding.F insort [] = sorted_list_of_set" by (simp only: sorted_list_of_set_def)
qed
--- a/src/HOL/Matrix_LP/Matrix.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Matrix_LP/Matrix.thy Sun Sep 13 22:56:52 2015 +0200
@@ -1448,7 +1448,7 @@
definition "sup = combine_matrix sup"
instance
- by default (auto simp add: le_infI le_matrix_def inf_matrix_def sup_matrix_def)
+ by standard (auto simp add: le_infI le_matrix_def inf_matrix_def sup_matrix_def)
end
--- a/src/HOL/Matrix_LP/SparseMatrix.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Matrix_LP/SparseMatrix.thy Sun Sep 13 22:56:52 2015 +0200
@@ -120,8 +120,11 @@
done
instance matrix :: (lattice_ab_group_add_abs) lattice_ab_group_add_abs
-apply default
-unfolding abs_matrix_def .. (*FIXME move*)
+ apply standard
+ unfolding abs_matrix_def
+ apply rule
+ done
+ (*FIXME move*)
lemma sparse_row_vector_abs:
"sorted_spvec (v :: 'a::lattice_ring spvec) \<Longrightarrow> sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)"
--- a/src/HOL/MicroJava/J/State.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/MicroJava/J/State.thy Sun Sep 13 22:56:52 2015 +0200
@@ -191,7 +191,7 @@
begin
definition "HOL.equal (l :: loc') l' \<longleftrightarrow> l = l'"
-instance by default (simp add: equal_loc'_def)
+instance by standard (simp add: equal_loc'_def)
end
--- a/src/HOL/MicroJava/J/Type.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/MicroJava/J/Type.thy Sun Sep 13 22:56:52 2015 +0200
@@ -13,7 +13,7 @@
begin
definition "HOL.equal (cn :: cnam) cn' \<longleftrightarrow> cn = cn'"
-instance by default (simp add: equal_cnam_def)
+instance by standard (simp add: equal_cnam_def)
end
@@ -63,7 +63,7 @@
begin
definition "HOL.equal (vn :: vnam) vn' \<longleftrightarrow> vn = vn'"
-instance by default (simp add: equal_vnam_def)
+instance by standard (simp add: equal_vnam_def)
end
@@ -98,7 +98,7 @@
begin
definition "HOL.equal (M :: mname) M' \<longleftrightarrow> M = M'"
-instance by default (simp add: equal_mname_def)
+instance by standard (simp add: equal_mname_def)
end
--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Sun Sep 13 22:56:52 2015 +0200
@@ -315,7 +315,7 @@
by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun)
instance
- by default
+ by standard
(simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def
Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps
plus_cont const_bcontfun minus_cont scaleR_cont)
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sun Sep 13 22:56:52 2015 +0200
@@ -589,7 +589,7 @@
using enum_Suc[of 0] na[rule_format, OF \<open>enum 1 \<in> s - {a}\<close>] \<open>a = enum 0\<close> by (auto simp: \<open>upd 0 = n\<close>)
show ?thesis
- proof (rule ksimplex.intros, default)
+ proof (rule ksimplex.intros, standard)
show "bij_betw (upd\<circ>Suc) {..< n} {..< n}" by fact
show "base(n := p) \<in> {..<n} \<rightarrow> {..<p}" "\<And>i. n\<le>i \<Longrightarrow> (base(n := p)) i = p"
using base base_out by (auto simp: Pi_iff)
@@ -620,7 +620,7 @@
def u \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> n | Suc i \<Rightarrow> upd i"
have "ksimplex p (Suc n) (s' \<union> {b})"
- proof (rule ksimplex.intros, default)
+ proof (rule ksimplex.intros, standard)
show "b \<in> {..<Suc n} \<rightarrow> {..<p}"
using base \<open>0 < p\<close> unfolding lessThan_Suc b_def by (auto simp: PiE_iff)
show "\<And>i. Suc n \<le> i \<Longrightarrow> b i = p"
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Sep 13 22:56:52 2015 +0200
@@ -73,7 +73,7 @@
end
instance vec:: (order, finite) order
- by default (auto simp: less_eq_vec_def less_vec_def vec_eq_iff
+ by standard (auto simp: less_eq_vec_def less_vec_def vec_eq_iff
intro: order.trans order.antisym order.strict_implies_order)
instance vec :: (linorder, cart_one) linorder
@@ -183,26 +183,26 @@
subsection \<open>Some frequently useful arithmetic lemmas over vectors.\<close>
instance vec :: (semigroup_mult, finite) semigroup_mult
- by default (vector mult.assoc)
+ by standard (vector mult.assoc)
instance vec :: (monoid_mult, finite) monoid_mult
- by default vector+
+ by standard vector+
instance vec :: (ab_semigroup_mult, finite) ab_semigroup_mult
- by default (vector mult.commute)
+ by standard (vector mult.commute)
instance vec :: (comm_monoid_mult, finite) comm_monoid_mult
- by default vector
+ by standard vector
instance vec :: (semiring, finite) semiring
- by default (vector field_simps)+
+ by standard (vector field_simps)+
instance vec :: (semiring_0, finite) semiring_0
- by default (vector field_simps)+
+ by standard (vector field_simps)+
instance vec :: (semiring_1, finite) semiring_1
- by default vector
+ by standard vector
instance vec :: (comm_semiring, finite) comm_semiring
- by default (vector field_simps)+
+ by standard (vector field_simps)+
instance vec :: (comm_semiring_0, finite) comm_semiring_0 ..
instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
@@ -215,7 +215,7 @@
instance vec :: (ring_1, finite) ring_1 ..
instance vec :: (real_algebra, finite) real_algebra
- by default (simp_all add: vec_eq_iff)
+ by standard (simp_all add: vec_eq_iff)
instance vec :: (real_algebra_1, finite) real_algebra_1 ..
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun Sep 13 22:56:52 2015 +0200
@@ -139,7 +139,7 @@
[simp]: "Basis = {1::real}"
instance
- by default auto
+ by standard auto
end
@@ -155,7 +155,7 @@
"Basis = {1, ii}"
instance
- by default (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm)
+ by standard (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm)
end
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Sun Sep 13 22:56:52 2015 +0200
@@ -53,7 +53,7 @@
qed
instance ereal :: second_countable_topology
-proof (default, intro exI conjI)
+proof (standard, intro exI conjI)
let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"
show "countable ?B"
by (auto intro: countable_rat)
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sun Sep 13 22:56:52 2015 +0200
@@ -95,30 +95,30 @@
unfolding uminus_vec_def by simp
instance vec :: (semigroup_add, finite) semigroup_add
- by default (simp add: vec_eq_iff add.assoc)
+ by standard (simp add: vec_eq_iff add.assoc)
instance vec :: (ab_semigroup_add, finite) ab_semigroup_add
- by default (simp add: vec_eq_iff add.commute)
+ by standard (simp add: vec_eq_iff add.commute)
instance vec :: (monoid_add, finite) monoid_add
- by default (simp_all add: vec_eq_iff)
+ by standard (simp_all add: vec_eq_iff)
instance vec :: (comm_monoid_add, finite) comm_monoid_add
- by default (simp add: vec_eq_iff)
+ by standard (simp add: vec_eq_iff)
instance vec :: (cancel_semigroup_add, finite) cancel_semigroup_add
- by default (simp_all add: vec_eq_iff)
+ by standard (simp_all add: vec_eq_iff)
instance vec :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add
- by default (simp_all add: vec_eq_iff diff_diff_eq)
+ by standard (simp_all add: vec_eq_iff diff_diff_eq)
instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
instance vec :: (group_add, finite) group_add
- by default (simp_all add: vec_eq_iff)
+ by standard (simp_all add: vec_eq_iff)
instance vec :: (ab_group_add, finite) ab_group_add
- by default (simp_all add: vec_eq_iff)
+ by standard (simp_all add: vec_eq_iff)
subsection \<open>Real vector space\<close>
@@ -132,7 +132,7 @@
unfolding scaleR_vec_def by simp
instance
- by default (simp_all add: vec_eq_iff scaleR_left_distrib scaleR_right_distrib)
+ by standard (simp_all add: vec_eq_iff scaleR_left_distrib scaleR_right_distrib)
end
@@ -412,7 +412,7 @@
by (rule member_le_setL2) simp_all
lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
-apply default
+apply standard
apply (rule vector_add_component)
apply (rule vector_scaleR_component)
apply (rule_tac x="1" in exI, simp add: norm_nth_le)
--- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Sun Sep 13 22:56:52 2015 +0200
@@ -17,20 +17,20 @@
begin
subclass order
- by default
+ by standard
(auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans)
subclass ordered_ab_group_add_abs
- by default (auto simp: eucl_le inner_add_left eucl_abs abs_leI)
+ by standard (auto simp: eucl_le inner_add_left eucl_abs abs_leI)
subclass ordered_real_vector
- by default (auto simp: eucl_le intro!: mult_left_mono mult_right_mono)
+ by standard (auto simp: eucl_le intro!: mult_left_mono mult_right_mono)
subclass lattice
- by default (auto simp: eucl_inf eucl_sup eucl_le)
+ by standard (auto simp: eucl_inf eucl_sup eucl_le)
subclass distrib_lattice
- by default (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI)
+ by standard (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI)
subclass conditionally_complete_lattice
proof
@@ -152,7 +152,7 @@
by (auto)
instance real :: ordered_euclidean_space
- by default (auto simp: INF_def SUP_def)
+ by standard (auto simp: INF_def SUP_def)
lemma in_Basis_prod_iff:
fixes i::"'a::euclidean_space*'b::euclidean_space"
@@ -168,7 +168,7 @@
end
instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
- by default
+ by standard
(auto intro!: add_mono simp add: euclidean_representation_setsum' Ball_def inner_prod_def
in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def
inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a]
@@ -281,7 +281,7 @@
definition "abs x = (\<chi> i. abs (x $ i))"
instance
- apply default
+ apply standard
unfolding euclidean_representation_setsum'
apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis
Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left
--- a/src/HOL/Nat.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Nat.thy Sun Sep 13 22:56:52 2015 +0200
@@ -529,7 +529,7 @@
end
instance nat :: no_top
- by default (auto intro: less_Suc_eq_le [THEN iffD2])
+ by standard (auto intro: less_Suc_eq_le [THEN iffD2])
subsubsection \<open>Introduction properties\<close>
--- a/src/HOL/Nominal/Examples/Pattern.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy Sun Sep 13 22:56:52 2015 +0200
@@ -62,7 +62,7 @@
by (simp add: supp_def Collect_disj_eq del: disj_not1)
instance pat :: pt_name
-proof (default, goal_cases)
+proof (standard, goal_cases)
case (1 x)
show ?case by (induct x) simp_all
next
@@ -74,7 +74,7 @@
qed
instance pat :: fs_name
-proof (default, goal_cases)
+proof (standard, goal_cases)
case (1 x)
show ?case by (induct x) (simp_all add: fin_supp)
qed
--- a/src/HOL/Num.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Num.thy Sun Sep 13 22:56:52 2015 +0200
@@ -106,7 +106,7 @@
"m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
instance
- by (default, auto simp add: less_num_def less_eq_num_def num_eq_iff)
+ by standard (auto simp add: less_num_def less_eq_num_def num_eq_iff)
end
--- a/src/HOL/Orderings.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Orderings.thy Sun Sep 13 22:56:52 2015 +0200
@@ -196,7 +196,7 @@
by (auto simp add: less_le_not_le intro: antisym)
sublocale order!: ordering less_eq less + dual_order!: ordering greater_eq greater
- by default (auto intro: antisym order_trans simp add: less_le)
+ by standard (auto intro: antisym order_trans simp add: less_le)
text \<open>Reflexivity.\<close>
@@ -1197,7 +1197,7 @@
begin
sublocale bot!: ordering_top greater_eq greater bot
- by default (fact bot_least)
+ by standard (fact bot_least)
lemma le_bot:
"a \<le> \<bottom> \<Longrightarrow> a = \<bottom>"
@@ -1225,7 +1225,7 @@
begin
sublocale top!: ordering_top less_eq less top
- by default (fact top_greatest)
+ by standard (fact top_greatest)
lemma top_le:
"\<top> \<le> a \<Longrightarrow> a = \<top>"
--- a/src/HOL/Probability/Binary_Product_Measure.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Sun Sep 13 22:56:52 2015 +0200
@@ -702,7 +702,7 @@
proof (rule measure_eqI)
interpret A: finite_measure "count_space A" by (rule finite_measure_count_space) fact
interpret B: finite_measure "count_space B" by (rule finite_measure_count_space) fact
- interpret P: pair_sigma_finite "count_space A" "count_space B" by default
+ interpret P: pair_sigma_finite "count_space A" "count_space B" ..
show eq: "sets ?P = sets ?C"
by (simp add: sets_pair_measure sigma_sets_pair_measure_generator_finite A B)
fix X assume X: "X \<in> sets ?P"
@@ -890,7 +890,7 @@
proof -
interpret M1: sigma_finite_measure M1 by fact
interpret M2: sigma_finite_measure M2 by fact
- interpret pair_sigma_finite M1 M2 by default
+ interpret pair_sigma_finite M1 M2 ..
from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
let ?P = "M1 \<Otimes>\<^sub>M M2"
--- a/src/HOL/Probability/Bochner_Integration.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy Sun Sep 13 22:56:52 2015 +0200
@@ -2549,7 +2549,7 @@
assumes "integrable (M1 \<Otimes>\<^sub>M M2) f"
shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x))"
proof -
- interpret Q: pair_sigma_finite M2 M1 by default
+ interpret Q: pair_sigma_finite M2 M1 ..
have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
show ?thesis unfolding *
by (rule integrable_distr[OF measurable_pair_swap'])
@@ -2560,7 +2560,7 @@
fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow> integrable (M1 \<Otimes>\<^sub>M M2) f"
proof -
- interpret Q: pair_sigma_finite M2 M1 by default
+ interpret Q: pair_sigma_finite M2 M1 ..
from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f]
show ?thesis by auto
qed
@@ -2751,7 +2751,7 @@
and integrable_snd: "integrable M2 (\<lambda>y. \<integral>x. f x y \<partial>M1)" (is "?INT")
and integral_snd: "(\<integral>y. (\<integral>x. f x y \<partial>M1) \<partial>M2) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (split f)" (is "?EQ")
proof -
- interpret Q: pair_sigma_finite M2 M1 by default
+ interpret Q: pair_sigma_finite M2 M1 ..
have Q_int: "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x, y). f y x)"
using f unfolding integrable_product_swap_iff[symmetric] by simp
show ?AE using Q.AE_integrable_fst'[OF Q_int] by simp
@@ -2780,11 +2780,11 @@
and f: "integrable (Pi\<^sub>M (I \<union> J) M) f"
shows "integral\<^sup>L (Pi\<^sub>M (I \<union> J) M) f = (\<integral>x. (\<integral>y. f (merge I J (x, y)) \<partial>Pi\<^sub>M J M) \<partial>Pi\<^sub>M I M)"
proof -
- interpret I: finite_product_sigma_finite M I by default fact
- interpret J: finite_product_sigma_finite M J by default fact
+ interpret I: finite_product_sigma_finite M I by standard fact
+ interpret J: finite_product_sigma_finite M J by standard fact
have "finite (I \<union> J)" using fin by auto
- interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
- interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default
+ interpret IJ: finite_product_sigma_finite M "I \<union> J" by standard fact
+ interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" ..
let ?M = "merge I J"
let ?f = "\<lambda>x. f (?M x)"
from f have f_borel: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
@@ -2830,7 +2830,7 @@
assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
shows "integrable (Pi\<^sub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
proof (unfold integrable_iff_bounded, intro conjI)
- interpret finite_product_sigma_finite M I by default fact
+ interpret finite_product_sigma_finite M I by standard fact
show "?f \<in> borel_measurable (Pi\<^sub>M I M)"
using assms by simp
@@ -2859,7 +2859,7 @@
then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
integrable (Pi\<^sub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
by (intro product_integrable_setprod insert(4)) (auto intro: finite_subset)
- interpret I: finite_product_sigma_finite M I by default fact
+ interpret I: finite_product_sigma_finite M I by standard fact
have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
using `i \<notin> I` by (auto intro!: setprod.cong)
show ?case
--- a/src/HOL/Probability/Embed_Measure.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Embed_Measure.thy Sun Sep 13 22:56:52 2015 +0200
@@ -169,7 +169,7 @@
from A_props and inj have "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
by (intro ballI, subst emeasure_embed_measure)
(auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
- ultimately show ?thesis by - (default, blast)
+ ultimately show ?thesis by - (standard, blast)
qed
lemma embed_measure_count_space':
--- a/src/HOL/Probability/Finite_Product_Measure.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Sun Sep 13 22:56:52 2015 +0200
@@ -764,9 +764,9 @@
"finite I \<Longrightarrow> (\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> emeasure (PiM I M) (Pi\<^sub>E I A) = (\<Prod>i\<in>I. emeasure (M i) (A i))"
proof (induct I arbitrary: A rule: finite_induct)
case (insert i I)
- interpret finite_product_sigma_finite M I by default fact
+ interpret finite_product_sigma_finite M I by standard fact
have "finite (insert i I)" using `finite I` by auto
- interpret I': finite_product_sigma_finite M "insert i I" by default fact
+ interpret I': finite_product_sigma_finite M "insert i I" by standard fact
let ?h = "(\<lambda>(f, y). f(i := y))"
let ?P = "distr (Pi\<^sub>M I M \<Otimes>\<^sub>M M i) (Pi\<^sub>M (insert i I) M) ?h"
@@ -821,7 +821,7 @@
assumes "finite I"
shows "sigma_finite_measure (PiM I M)"
proof
- interpret finite_product_sigma_finite M I by default fact
+ interpret finite_product_sigma_finite M I by standard fact
obtain F where F: "\<And>j. countable (F j)" "\<And>j f. f \<in> F j \<Longrightarrow> f \<in> sets (M j)"
"\<And>j f. f \<in> F j \<Longrightarrow> emeasure (M j) f \<noteq> \<infinity>" and
@@ -846,7 +846,7 @@
assumes pos: "0 \<le> f (\<lambda>k. undefined)"
shows "integral\<^sup>N (Pi\<^sub>M {} M) f = f (\<lambda>k. undefined)"
proof -
- interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI)
+ interpret finite_product_sigma_finite M "{}" by standard (fact finite.emptyI)
have "\<And>A. emeasure (Pi\<^sub>M {} M) (Pi\<^sub>E {} A) = 1"
using assms by (subst measure_times) auto
then show ?thesis
@@ -864,11 +864,11 @@
shows "distr (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \<union> J) M) (merge I J) = Pi\<^sub>M (I \<union> J) M"
(is "?D = ?P")
proof -
- interpret I: finite_product_sigma_finite M I by default fact
- interpret J: finite_product_sigma_finite M J by default fact
+ interpret I: finite_product_sigma_finite M I by standard fact
+ interpret J: finite_product_sigma_finite M J by standard fact
have "finite (I \<union> J)" using fin by auto
- interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
- interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default
+ interpret IJ: finite_product_sigma_finite M "I \<union> J" by standard fact
+ interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard
let ?g = "merge I J"
from IJ.sigma_finite_pairs obtain F where
@@ -928,9 +928,9 @@
shows "integral\<^sup>N (Pi\<^sub>M (I \<union> J) M) f =
(\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^sub>M J M)) \<partial>(Pi\<^sub>M I M))"
proof -
- interpret I: finite_product_sigma_finite M I by default fact
- interpret J: finite_product_sigma_finite M J by default fact
- interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default
+ interpret I: finite_product_sigma_finite M I by standard fact
+ interpret J: finite_product_sigma_finite M J by standard fact
+ interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard
have P_borel: "(\<lambda>x. f (merge I J x)) \<in> borel_measurable (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)"
using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
show ?thesis
@@ -944,7 +944,7 @@
lemma (in product_sigma_finite) distr_singleton:
"distr (Pi\<^sub>M {i} M) (M i) (\<lambda>x. x i) = M i" (is "?D = _")
proof (intro measure_eqI[symmetric])
- interpret I: finite_product_sigma_finite M "{i}" by default simp
+ interpret I: finite_product_sigma_finite M "{i}" by standard simp
fix A assume A: "A \<in> sets (M i)"
then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M {i} M) = (\<Pi>\<^sub>E i\<in>{i}. A)"
using sets.sets_into_space by (auto simp: space_PiM)
@@ -957,7 +957,7 @@
assumes f: "f \<in> borel_measurable (M i)"
shows "integral\<^sup>N (Pi\<^sub>M {i} M) (\<lambda>x. f (x i)) = integral\<^sup>N (M i) f"
proof -
- interpret I: finite_product_sigma_finite M "{i}" by default simp
+ interpret I: finite_product_sigma_finite M "{i}" by standard simp
from f show ?thesis
apply (subst distr_singleton[symmetric])
apply (subst nn_integral_distr[OF measurable_component_singleton])
@@ -970,8 +970,8 @@
and f: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (x(i := y)) \<partial>(M i)) \<partial>(Pi\<^sub>M I M))"
proof -
- interpret I: finite_product_sigma_finite M I by default auto
- interpret i: finite_product_sigma_finite M "{i}" by default auto
+ interpret I: finite_product_sigma_finite M I by standard auto
+ interpret i: finite_product_sigma_finite M "{i}" by standard auto
have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
using f by auto
show ?thesis
@@ -1008,7 +1008,7 @@
using assms proof induct
case (insert i I)
note `finite I`[intro, simp]
- interpret I: finite_product_sigma_finite M I by default auto
+ interpret I: finite_product_sigma_finite M I by standard auto
have *: "\<And>x y. (\<Prod>j\<in>I. f j (if j = i then y else x j)) = (\<Prod>j\<in>I. f j (x j))"
using insert by (auto intro!: setprod.cong)
have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow> (\<lambda>x. (\<Prod>i\<in>J. f i (x i))) \<in> borel_measurable (Pi\<^sub>M J M)"
@@ -1044,7 +1044,7 @@
lemma (in product_sigma_finite) distr_component:
"distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P")
proof (intro measure_eqI[symmetric])
- interpret I: finite_product_sigma_finite M "{i}" by default simp
+ interpret I: finite_product_sigma_finite M "{i}" by standard simp
have eq: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x"
by (auto simp: extensional_def restrict_def)
@@ -1068,8 +1068,8 @@
and emeasure_fold_measurable:
"(\<lambda>x. emeasure (Pi\<^sub>M J M) ((\<lambda>y. merge I J (x, y)) -` A \<inter> space (Pi\<^sub>M J M))) \<in> borel_measurable (Pi\<^sub>M I M)" (is ?B)
proof -
- interpret I: finite_product_sigma_finite M I by default fact
- interpret J: finite_product_sigma_finite M J by default fact
+ interpret I: finite_product_sigma_finite M I by standard fact
+ interpret J: finite_product_sigma_finite M J by standard fact
interpret IJ: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" ..
have merge: "merge I J -` A \<inter> space (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M) \<in> sets (Pi\<^sub>M I M \<Otimes>\<^sub>M Pi\<^sub>M J M)"
by (intro measurable_sets[OF _ A] measurable_merge assms)
--- a/src/HOL/Probability/Giry_Monad.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy Sun Sep 13 22:56:52 2015 +0200
@@ -25,7 +25,7 @@
proof
show "emeasure M (space M) \<noteq> \<infinity>" using * by auto
qed
- show "subprob_space M" by default fact+
+ show "subprob_space M" by standard fact+
qed
lemma prob_space_imp_subprob_space:
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Sun Sep 13 22:56:52 2015 +0200
@@ -50,8 +50,8 @@
have "finite (K - J)" using K by auto
- interpret J: finite_product_prob_space M J by default fact+
- interpret KmJ: finite_product_prob_space M "K - J" by default fact+
+ interpret J: finite_product_prob_space M J by standard fact+
+ interpret KmJ: finite_product_prob_space M "K - J" by standard fact+
have "\<mu>G Z = emeasure (Pi\<^sub>M (J \<union> (K - J)) M) (emb (J \<union> (K - J)) K X)"
using K J by simp
@@ -84,7 +84,7 @@
proof (rule G.caratheodory_empty_continuous[OF positive_mu_G additive_mu_G])
fix A assume "A \<in> ?G"
with generatorE guess J X . note JX = this
- interpret JK: finite_product_prob_space M J by default fact+
+ interpret JK: finite_product_prob_space M J by standard fact+
from JX show "\<mu>G A \<noteq> \<infinity>" by simp
next
fix A assume A: "range A \<subseteq> ?G" "decseq A" "(\<Inter>i. A i) = {}"
@@ -113,7 +113,7 @@
have J_mono: "\<And>n m. n \<le> m \<Longrightarrow> J n \<subseteq> J m"
unfolding J_def by force
- interpret J: finite_product_prob_space M "J i" for i by default fact+
+ interpret J: finite_product_prob_space M "J i" for i by standard fact+
have a_le_1: "?a \<le> 1"
using mu_G_spec[of "J 0" "A 0" "X 0"] J A_eq
@@ -124,7 +124,7 @@
{ fix Z k assume Z: "range Z \<subseteq> ?G" "decseq Z" "\<forall>n. ?a / 2^k \<le> \<mu>G (Z n)"
then have Z_sets: "\<And>n. Z n \<in> ?G" by auto
fix J' assume J': "J' \<noteq> {}" "finite J'" "J' \<subseteq> I"
- interpret J': finite_product_prob_space M J' by default fact+
+ interpret J': finite_product_prob_space M J' by standard fact+
let ?q = "\<lambda>n y. \<mu>G (?M J' (Z n) y)"
let ?Q = "\<lambda>n. ?q n -` {?a / 2^(k+1) ..} \<inter> space (Pi\<^sub>M J' M)"
--- a/src/HOL/Probability/Information.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Information.thy Sun Sep 13 22:56:52 2015 +0200
@@ -311,7 +311,7 @@
shows "0 \<le> KL_divergence b (density M f) (density M g)"
proof -
interpret Mf: prob_space "density M f" by fact
- interpret Mf: information_space "density M f" b by default fact
+ interpret Mf: information_space "density M f" b by standard fact
have eq: "density (density M f) (\<lambda>x. g x / f x) = density M g" (is "?DD = _")
using f g ac by (subst density_density_divide) simp_all
@@ -443,8 +443,8 @@
by (rule prob_space_distr) fact
interpret Y: prob_space "distr M T Y"
by (rule prob_space_distr) fact
- interpret XY: pair_prob_space "distr M S X" "distr M T Y" by default
- interpret P: information_space P b unfolding P_def by default (rule b_gt_1)
+ interpret XY: pair_prob_space "distr M S X" "distr M T Y" by standard
+ interpret P: information_space P b unfolding P_def by standard (rule b_gt_1)
interpret Q: prob_space Q unfolding Q_def
by (rule prob_space_distr) simp
@@ -770,7 +770,7 @@
interpret X: prob_space "distr M S X"
using D(1) by (rule prob_space_distr)
- have sf: "sigma_finite_measure (distr M S X)" by default
+ have sf: "sigma_finite_measure (distr M S X)" by standard
show ?thesis
using D
apply (subst eq_commute)
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Sun Sep 13 22:56:52 2015 +0200
@@ -2454,7 +2454,7 @@
lemma (in finite_measure) finite_measure_restricted:
"S \<in> sets M \<Longrightarrow> finite_measure (density M (indicator S))"
- by default (simp add: emeasure_restricted)
+ by standard (simp add: emeasure_restricted)
lemma emeasure_density_const:
"A \<in> sets M \<Longrightarrow> 0 \<le> c \<Longrightarrow> emeasure (density M (\<lambda>_. c)) A = c * emeasure M A"
--- a/src/HOL/Probability/Probability_Mass_Function.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Sun Sep 13 22:56:52 2015 +0200
@@ -653,7 +653,7 @@
measure (density (count_space UNIV) (ereal \<circ> f)) {x} \<noteq> 0"
by (simp add: AE_density nonneg measure_def emeasure_density max_def)
show "prob_space (density (count_space UNIV) (ereal \<circ> f))"
- by default (simp add: emeasure_density prob)
+ by standard (simp add: emeasure_density prob)
qed simp
lemma pmf_embed_pmf: "pmf embed_pmf x = f x"
--- a/src/HOL/Probability/Probability_Measure.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy Sun Sep 13 22:56:52 2015 +0200
@@ -20,7 +20,7 @@
proof
show "emeasure M (space M) \<noteq> \<infinity>" using * by simp
qed
- show "prob_space M" by default fact
+ show "prob_space M" by standard fact
qed
lemma prob_space_imp_sigma_finite: "prob_space M \<Longrightarrow> sigma_finite_measure M"
@@ -626,7 +626,7 @@
proof safe
interpret S: sigma_finite_measure S by fact
interpret T: sigma_finite_measure T by fact
- interpret ST: pair_sigma_finite S T by default
+ interpret ST: pair_sigma_finite S T ..
from ST.sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('b \<times> 'c) set" .. note F = this
let ?E = "{a \<times> b |a b. a \<in> sets S \<and> b \<in> sets T}"
@@ -666,8 +666,8 @@
proof -
interpret S: sigma_finite_measure S by fact
interpret T: sigma_finite_measure T by fact
- interpret ST: pair_sigma_finite S T by default
- interpret TS: pair_sigma_finite T S by default
+ interpret ST: pair_sigma_finite S T ..
+ interpret TS: pair_sigma_finite T S ..
note Pxy[measurable]
show ?thesis
@@ -715,7 +715,7 @@
proof safe
interpret S: sigma_finite_measure S by fact
interpret T: sigma_finite_measure T by fact
- interpret ST: pair_sigma_finite S T by default
+ interpret ST: pair_sigma_finite S T ..
note Pxy[measurable]
show X: "X \<in> measurable M S" by simp
@@ -792,7 +792,7 @@
proof safe
interpret S: sigma_finite_measure S by fact
interpret T: sigma_finite_measure T by fact
- interpret ST: pair_sigma_finite S T by default
+ interpret ST: pair_sigma_finite S T ..
interpret X: prob_space "density S Px"
unfolding distributed_distr_eq_density[OF X, symmetric]
@@ -1133,7 +1133,7 @@
qed
lemma prob_space_uniform_count_measure: "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> prob_space (uniform_count_measure A)"
- by default (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def)
+ by standard (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def)
lemma (in prob_space) measure_uniform_measure_eq_cond_prob:
assumes [measurable]: "Measurable.pred M P" "Measurable.pred M Q"
--- a/src/HOL/Probability/Radon_Nikodym.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Sun Sep 13 22:56:52 2015 +0200
@@ -993,7 +993,7 @@
note A_in_sets = this
show "sigma_finite_measure ?N"
- proof (default, intro exI conjI ballI)
+ proof (standard, intro exI conjI ballI)
show "countable (range (\<lambda>(i, j). A i \<inter> Q j))"
by auto
show "range (\<lambda>(i, j). A i \<inter> Q j) \<subseteq> sets (density M f)"
--- a/src/HOL/Probability/Sigma_Algebra.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Sun Sep 13 22:56:52 2015 +0200
@@ -1333,7 +1333,7 @@
assumes "N \<subseteq> M"
shows "dynkin \<Omega> N \<subseteq> M"
proof -
- have "dynkin_system \<Omega> M" by default
+ have "dynkin_system \<Omega> M" ..
then have "dynkin_system \<Omega> M"
using assms unfolding dynkin_system_def dynkin_system_axioms_def subset_class_def by simp
with `N \<subseteq> M` show ?thesis by (auto simp add: dynkin_def)
@@ -1432,7 +1432,7 @@
using closed by (rule sigma_algebra_sigma_sets)
from compl[OF _ empty] closed have space: "P \<Omega>" by simp
interpret dynkin_system \<Omega> ?D
- by default (auto dest: sets_into_space intro!: space compl union)
+ by standard (auto dest: sets_into_space intro!: space compl union)
have "sigma_sets \<Omega> G = ?D"
by (rule dynkin_lemma) (auto simp: basic `Int_stable G`)
with A show ?thesis by auto
@@ -1967,7 +1967,7 @@
assume "\<not> (\<forall>i\<in>I. \<mu> i = 0)"
moreover
have "measure_space (space M) (sets M) \<mu>'"
- using ms unfolding measure_space_def by auto default
+ using ms unfolding measure_space_def by auto standard
with ms eq have "\<exists>\<mu>'. P \<mu>'"
unfolding P_def
by (intro exI[of _ \<mu>']) (auto simp add: M space_extend_measure sets_extend_measure)
--- a/src/HOL/Probability/Stream_Space.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/Stream_Space.thy Sun Sep 13 22:56:52 2015 +0200
@@ -160,7 +160,7 @@
lemma (in prob_space) prob_space_stream_space: "prob_space (stream_space M)"
proof -
- interpret product_prob_space "\<lambda>_. M" UNIV by default
+ interpret product_prob_space "\<lambda>_. M" UNIV ..
show ?thesis
by (subst stream_space_eq_distr) (auto intro!: P.prob_space_distr)
qed
@@ -169,10 +169,8 @@
assumes [measurable]: "f \<in> borel_measurable (stream_space M)"
shows "(\<integral>\<^sup>+X. f X \<partial>stream_space M) = (\<integral>\<^sup>+x. (\<integral>\<^sup>+X. f (x ## X) \<partial>stream_space M) \<partial>M)"
proof -
- interpret S: sequence_space M
- by default
- interpret P: pair_sigma_finite M "\<Pi>\<^sub>M i::nat\<in>UNIV. M"
- by default
+ interpret S: sequence_space M ..
+ interpret P: pair_sigma_finite M "\<Pi>\<^sub>M i::nat\<in>UNIV. M" ..
have "(\<integral>\<^sup>+X. f X \<partial>stream_space M) = (\<integral>\<^sup>+X. f (to_stream X) \<partial>S.S)"
by (subst stream_space_eq_distr) (simp add: nn_integral_distr)
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Sun Sep 13 22:56:52 2015 +0200
@@ -399,7 +399,7 @@
(insert n_gt_3, auto simp: dc_crypto intro: exI[of _ "replicate n True"])
sublocale dining_cryptographers_space \<subseteq> information_space "uniform_count_measure dc_crypto" 2
- by default auto
+ by standard auto
notation (in dining_cryptographers_space)
mutual_information_Pow ("\<I>'( _ ; _ ')")
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Sun Sep 13 22:56:52 2015 +0200
@@ -125,10 +125,10 @@
by (auto intro!: setsum_nonneg)
sublocale finite_information \<subseteq> prob_space "point_measure \<Omega> p"
- by default (simp add: one_ereal_def emeasure_point_measure_finite)
+ by standard (simp add: one_ereal_def emeasure_point_measure_finite)
sublocale finite_information \<subseteq> information_space "point_measure \<Omega> p" b
- by default simp
+ by standard simp
lemma (in finite_information) \<mu>'_eq: "A \<subseteq> \<Omega> \<Longrightarrow> prob A = setsum p A"
by (auto simp: measure_point_measure)
@@ -150,7 +150,7 @@
end
sublocale koepf_duermuth \<subseteq> finite_information msgs P b
-proof default
+proof
show "finite msgs" unfolding msgs_def
using finite_lists_length_eq[OF M.finite_space, of n]
by auto
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Sun Sep 13 22:56:52 2015 +0200
@@ -478,8 +478,8 @@
fixes R
assumes "R x y --> R y x --> x = y"
-interpretation equal : antisym "op =" by default simp
-interpretation order_nat : antisym "op <= :: nat => _ => _" by default simp
+interpretation equal : antisym "op =" by standard simp
+interpretation order_nat : antisym "op <= :: nat => _ => _" by standard simp
lemma (in antisym)
"R x y --> R y z --> R x z"
--- a/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy Sun Sep 13 22:56:52 2015 +0200
@@ -91,7 +91,7 @@
datatype ('a::finite, 'b::finite) F = F 'a | F2 'b
-instance T :: (finite) finite by (default, transfer, auto)
+instance T :: (finite) finite by standard (transfer, auto)
lift_definition(code_dt) f17 :: "bool \<Rightarrow> (bool T, 'b::finite) F" is "\<lambda>b. F b" by auto
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Sun Sep 13 22:56:52 2015 +0200
@@ -188,8 +188,7 @@
"(sup :: int \<Rightarrow> int \<Rightarrow> int) = max"
instance
- by default
- (auto simp add: inf_int_def sup_int_def max_min_distrib2)
+ by standard (auto simp add: inf_int_def sup_int_def max_min_distrib2)
end
--- a/src/HOL/Real_Vector_Spaces.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Sun Sep 13 22:56:52 2015 +0200
@@ -1294,7 +1294,7 @@
assumes "\<And>x y. f (x + y) = f x + f y"
assumes "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
shows "linear f"
- by default (rule assms)+
+ by standard (rule assms)+
locale bounded_linear = linear f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" +
assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
@@ -1334,7 +1334,7 @@
assumes "\<And>r x. f (scaleR r x) = scaleR r (f x)"
assumes "\<And>x. norm (f x) \<le> norm x * K"
shows "bounded_linear f"
- by default (fast intro: assms)+
+ by standard (fast intro: assms)+
locale bounded_bilinear =
fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector]
@@ -1415,10 +1415,10 @@
end
lemma bounded_linear_ident[simp]: "bounded_linear (\<lambda>x. x)"
- by default (auto intro!: exI[of _ 1])
+ by standard (auto intro!: exI[of _ 1])
lemma bounded_linear_zero[simp]: "bounded_linear (\<lambda>x. 0)"
- by default (auto intro!: exI[of _ 1])
+ by standard (auto intro!: exI[of _ 1])
lemma bounded_linear_add:
assumes "bounded_linear f"
@@ -1859,7 +1859,7 @@
class banach = real_normed_vector + complete_space
-instance real :: banach by default
+instance real :: banach ..
lemma tendsto_at_topI_sequentially:
fixes f :: "real \<Rightarrow> 'b::first_countable_topology"
--- a/src/HOL/Relation.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Relation.thy Sun Sep 13 22:56:52 2015 +0200
@@ -1116,7 +1116,7 @@
assumes "finite A"
shows "Id_on A = Finite_Set.fold (\<lambda>x. Set.insert (Pair x x)) {} A"
proof -
- interpret comp_fun_commute "\<lambda>x. Set.insert (Pair x x)" by default auto
+ interpret comp_fun_commute "\<lambda>x. Set.insert (Pair x x)" by standard auto
show ?thesis using assms unfolding Id_on_def by (induct A) simp_all
qed
@@ -1126,7 +1126,7 @@
interpret comp_fun_idem Set.insert
by (fact comp_fun_idem_insert)
show ?thesis
- by default (auto simp add: fun_eq_iff comp_fun_commute split:prod.split)
+ by standard (auto simp add: fun_eq_iff comp_fun_commute split:prod.split)
qed
lemma Image_fold:
@@ -1148,7 +1148,7 @@
proof -
interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
show "comp_fun_commute (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A')"
- by default (auto simp add: fun_eq_iff split:prod.split)
+ by standard (auto simp add: fun_eq_iff split:prod.split)
qed
have *: "{x} O S = {(x', z). x' = fst x \<and> (snd x,z) \<in> S}" by (auto simp: relcomp_unfold intro!: exI)
show ?thesis unfolding *
@@ -1172,7 +1172,7 @@
have *: "\<And>a b A.
Finite_Set.fold (\<lambda>(w, z) A'. if b = w then Set.insert (a, z) A' else A') A S = {(a,b)} O S \<union> A"
by (auto simp: insert_relcomp_union_fold[OF assms] cong: if_cong)
- show ?thesis by default (auto simp: *)
+ show ?thesis by standard (auto simp: *)
qed
lemma relcomp_fold:
--- a/src/HOL/Topological_Spaces.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy Sun Sep 13 22:56:52 2015 +0200
@@ -212,7 +212,7 @@
lemma topological_space_generate_topology:
"class.topological_space (generate_topology S)"
- by default (auto intro: generate_topology.intros)
+ by standard (auto intro: generate_topology.intros)
subsection \<open>Order topologies\<close>
--- a/src/HOL/UNITY/Follows.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/UNITY/Follows.thy Sun Sep 13 22:56:52 2015 +0200
@@ -179,7 +179,7 @@
"(M'::'a multiset) \<le> M \<longleftrightarrow> M' #<=# M"
instance
- by default (auto simp add: less_eq_multiset_def less_multiset_def multiset_order.less_le_not_le add.commute multiset_order.add_right_mono)
+ by standard (auto simp add: less_eq_multiset_def less_multiset_def multiset_order.less_le_not_le add.commute multiset_order.add_right_mono)
end
lemma increasing_union:
--- a/src/HOL/UNITY/Guar.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/UNITY/Guar.thy Sun Sep 13 22:56:52 2015 +0200
@@ -17,7 +17,7 @@
begin
instance program :: (type) order
- by default (auto simp add: program_less_le dest: component_antisym intro: component_trans)
+ by standard (auto simp add: program_less_le dest: component_antisym intro: component_trans)
text{*Existential and Universal properties. I formalize the two-program
case, proving equivalence with Chandy and Sanders's n-ary definitions*}
--- a/src/HOL/Word/Word.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Word/Word.thy Sun Sep 13 22:56:52 2015 +0200
@@ -313,7 +313,7 @@
word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
instance
- by default (transfer, simp add: algebra_simps)+
+ by standard (transfer, simp add: algebra_simps)+
end
@@ -384,7 +384,7 @@
word_less_def: "a < b \<longleftrightarrow> uint a < uint b"
instance
- by default (auto simp: word_less_def word_le_def)
+ by standard (auto simp: word_less_def word_le_def)
end
@@ -1194,7 +1194,7 @@
by (fact word_less_def)
lemma signed_linorder: "class.linorder word_sle word_sless"
- by default (unfold word_sle_def word_sless_def, auto)
+ by standard (unfold word_sle_def word_sless_def, auto)
interpretation signed: linorder "word_sle" "word_sless"
by (rule signed_linorder)
@@ -2215,7 +2215,7 @@
subsection {* Cardinality, finiteness of set of words *}
instance word :: (len0) finite
- by (default, simp add: type_definition.univ [OF type_definition_word])
+ by standard (simp add: type_definition.univ [OF type_definition_word])
lemma card_word: "CARD('a::len0 word) = 2 ^ len_of TYPE('a)"
by (simp add: type_definition.card [OF type_definition_word] nat_power_eq)
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy Sun Sep 13 22:56:52 2015 +0200
@@ -88,7 +88,7 @@
"perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"
typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
- by (default) (auto simp: perms_def)
+ by standard (auto simp: perms_def)
text {*First we need some auxiliary lemmas.*}
lemma permsI [Pure.intro]:
@@ -153,13 +153,14 @@
unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm)
instance
- apply default
+ apply standard
unfolding Rep_perm_inject [symmetric]
unfolding minus_perm_def
unfolding Rep_perm_add
unfolding Rep_perm_uminus
unfolding Rep_perm_0
- by (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])
+ apply (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])
+ done
end
@@ -198,7 +199,7 @@
PERMUTE permute_atom
interpretation atom_permute: permute permute_atom
- by (default) (simp add: permute_atom_def Rep_perm_simps)+
+ by standard (simp_all add: permute_atom_def Rep_perm_simps)
text {*Permuting permutations.*}
definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where
@@ -208,7 +209,7 @@
PERMUTE permute_perm
interpretation perm_permute: permute permute_perm
- apply default
+ apply standard
unfolding permute_perm_def
apply simp
apply (simp only: diff_conv_add_uminus minus_add add.assoc)
--- a/src/HOL/ex/Dedekind_Real.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/ex/Dedekind_Real.thy Sun Sep 13 22:56:52 2015 +0200
@@ -1567,7 +1567,7 @@
"(sup :: real \<Rightarrow> real \<Rightarrow> real) = max"
instance
- by default (auto simp add: inf_real_def sup_real_def max_min_distrib2)
+ by standard (auto simp add: inf_real_def sup_real_def max_min_distrib2)
end