tuned proofs -- less legacy;
authorwenzelm
Sun Sep 13 22:56:52 2015 +0200 (2015-09-13)
changeset 611694de9ff3ea29a
parent 61168 dcdfb6355a05
child 61170 dee0aec271b7
tuned proofs -- less legacy;
src/Doc/Codegen/Adaptation.thy
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/RingHom.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/BNF_Fixpoint_Base.thy
src/HOL/Basic_BNF_LFPs.thy
src/HOL/Complete_Partial_Order.thy
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Enum.thy
src/HOL/Finite_Set.thy
src/HOL/GCD.thy
src/HOL/Groups.thy
src/HOL/Groups_Big.thy
src/HOL/HOL.thy
src/HOL/HOLCF/Bifinite.thy
src/HOL/HOLCF/Completion.thy
src/HOL/HOLCF/ConvexPD.thy
src/HOL/HOLCF/Deflation.thy
src/HOL/HOLCF/Discrete.thy
src/HOL/HOLCF/Domain.thy
src/HOL/HOLCF/Fun_Cpo.thy
src/HOL/HOLCF/Library/Defl_Bifinite.thy
src/HOL/HOLCF/Library/List_Predomain.thy
src/HOL/HOLCF/Library/Option_Cpo.thy
src/HOL/HOLCF/Library/Sum_Cpo.thy
src/HOL/HOLCF/LowerPD.thy
src/HOL/HOLCF/Map_Functions.thy
src/HOL/HOLCF/Pcpo.thy
src/HOL/HOLCF/Representable.thy
src/HOL/HOLCF/Universal.thy
src/HOL/HOLCF/UpperPD.thy
src/HOL/Int.thy
src/HOL/Lattices.thy
src/HOL/Lattices_Big.thy
src/HOL/Limits.thy
src/HOL/List.thy
src/HOL/Matrix_LP/Matrix.thy
src/HOL/Matrix_LP/SparseMatrix.thy
src/HOL/MicroJava/J/State.thy
src/HOL/MicroJava/J/Type.thy
src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy
src/HOL/Nat.thy
src/HOL/Nominal/Examples/Pattern.thy
src/HOL/Num.thy
src/HOL/Orderings.thy
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Embed_Measure.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Probability_Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Probability/Stream_Space.thy
src/HOL/Probability/ex/Dining_Cryptographers.thy
src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Relation.thy
src/HOL/Topological_Spaces.thy
src/HOL/UNITY/Follows.thy
src/HOL/UNITY/Guar.thy
src/HOL/Word/Word.thy
src/HOL/ex/Adhoc_Overloading_Examples.thy
src/HOL/ex/Dedekind_Real.thy
     1.1 --- a/src/Doc/Codegen/Adaptation.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/Doc/Codegen/Adaptation.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -346,7 +346,7 @@
     1.4  
     1.5  definition %quote "HOL.equal (x::bar) y \<longleftrightarrow> x = y"
     1.6  
     1.7 -instance %quote by default (simp add: equal_bar_def)
     1.8 +instance %quote by standard (simp add: equal_bar_def)
     1.9  
    1.10  end %quote (*<*)
    1.11  
     2.1 --- a/src/HOL/Algebra/AbelCoset.thy	Sun Sep 13 22:25:21 2015 +0200
     2.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Sun Sep 13 22:56:52 2015 +0200
     2.3 @@ -236,7 +236,7 @@
     2.4      by (rule a_normal)
     2.5  
     2.6    show "abelian_subgroup H G"
     2.7 -    by default (simp add: a_comm)
     2.8 +    by standard (simp add: a_comm)
     2.9  qed
    2.10  
    2.11  lemma abelian_subgroupI2:
     3.1 --- a/src/HOL/Algebra/Divisibility.thy	Sun Sep 13 22:25:21 2015 +0200
     3.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sun Sep 13 22:56:52 2015 +0200
     3.3 @@ -25,14 +25,14 @@
     3.4        and r_cancel: 
     3.5            "\<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"
     3.6    shows "monoid_cancel G"
     3.7 -    by default fact+
     3.8 +    by standard fact+
     3.9  
    3.10  lemma (in monoid_cancel) is_monoid_cancel:
    3.11    "monoid_cancel G"
    3.12    ..
    3.13  
    3.14  sublocale group \<subseteq> monoid_cancel
    3.15 -  by default simp_all
    3.16 +  by standard simp_all
    3.17  
    3.18  
    3.19  locale comm_monoid_cancel = monoid_cancel + comm_monoid
    3.20 @@ -3640,7 +3640,7 @@
    3.21  done
    3.22  
    3.23  sublocale factorial_monoid \<subseteq> primeness_condition_monoid
    3.24 -  by default (rule irreducible_is_prime)
    3.25 +  by standard (rule irreducible_is_prime)
    3.26  
    3.27  
    3.28  lemma (in factorial_monoid) primeness_condition:
    3.29 @@ -3649,10 +3649,10 @@
    3.30  
    3.31  lemma (in factorial_monoid) gcd_condition [simp]:
    3.32    shows "gcd_condition_monoid G"
    3.33 -  by default (rule gcdof_exists)
    3.34 +  by standard (rule gcdof_exists)
    3.35  
    3.36  sublocale factorial_monoid \<subseteq> gcd_condition_monoid
    3.37 -  by default (rule gcdof_exists)
    3.38 +  by standard (rule gcdof_exists)
    3.39  
    3.40  lemma (in factorial_monoid) division_weak_lattice [simp]:
    3.41    shows "weak_lattice (division_rel G)"
     4.1 --- a/src/HOL/Algebra/Group.thy	Sun Sep 13 22:25:21 2015 +0200
     4.2 +++ b/src/HOL/Algebra/Group.thy	Sun Sep 13 22:56:52 2015 +0200
     4.3 @@ -286,7 +286,8 @@
     4.4    qed
     4.5    then have carrier_subset_Units: "carrier G <= Units G"
     4.6      by (unfold Units_def) fast
     4.7 -  show ?thesis by default (auto simp: r_one m_assoc carrier_subset_Units)
     4.8 +  show ?thesis
     4.9 +    by standard (auto simp: r_one m_assoc carrier_subset_Units)
    4.10  qed
    4.11  
    4.12  lemma (in monoid) group_l_invI:
    4.13 @@ -730,7 +731,7 @@
    4.14    assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
    4.15        x \<otimes> y = y \<otimes> x"
    4.16    shows "comm_group G"
    4.17 -  by default (simp_all add: m_comm)
    4.18 +  by standard (simp_all add: m_comm)
    4.19  
    4.20  lemma comm_groupI:
    4.21    fixes G (structure)
    4.22 @@ -758,7 +759,7 @@
    4.23  
    4.24  theorem (in group) subgroups_partial_order:
    4.25    "partial_order \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
    4.26 -  by default simp_all
    4.27 +  by standard simp_all
    4.28  
    4.29  lemma (in group) subgroup_self:
    4.30    "subgroup (carrier G) G"
     5.1 --- a/src/HOL/Algebra/IntRing.thy	Sun Sep 13 22:25:21 2015 +0200
     5.2 +++ b/src/HOL/Algebra/IntRing.thy	Sun Sep 13 22:56:52 2015 +0200
     5.3 @@ -60,7 +60,7 @@
     5.4      and "pow \<Z> x n = x^n"
     5.5  proof -
     5.6    -- "Specification"
     5.7 -  show "monoid \<Z>" by default auto
     5.8 +  show "monoid \<Z>" by standard auto
     5.9    then interpret int: monoid \<Z> .
    5.10  
    5.11    -- "Carrier"
    5.12 @@ -76,7 +76,7 @@
    5.13    where "finprod \<Z> f A = setprod f A"
    5.14  proof -
    5.15    -- "Specification"
    5.16 -  show "comm_monoid \<Z>" by default auto
    5.17 +  show "comm_monoid \<Z>" by standard auto
    5.18    then interpret int: comm_monoid \<Z> .
    5.19  
    5.20    -- "Operations"
    5.21 @@ -94,7 +94,7 @@
    5.22      and int_finsum_eq: "finsum \<Z> f A = setsum f A"
    5.23  proof -
    5.24    -- "Specification"
    5.25 -  show "abelian_monoid \<Z>" by default auto
    5.26 +  show "abelian_monoid \<Z>" by standard auto
    5.27    then interpret int: abelian_monoid \<Z> .
    5.28  
    5.29    -- "Carrier"
    5.30 @@ -178,7 +178,7 @@
    5.31      and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)"
    5.32  proof -
    5.33    show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    5.34 -    by default simp_all
    5.35 +    by standard simp_all
    5.36    show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV"
    5.37      by simp
    5.38    show "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)"
    5.39 @@ -215,7 +215,7 @@
    5.40  
    5.41  interpretation int (* [unfolded UNIV] *) :
    5.42    total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>"
    5.43 -  by default clarsimp
    5.44 +  by standard clarsimp
    5.45  
    5.46  
    5.47  subsection {* Generated Ideals of @{text "\<Z>"} *}
     6.1 --- a/src/HOL/Algebra/Lattice.thy	Sun Sep 13 22:25:21 2015 +0200
     6.2 +++ b/src/HOL/Algebra/Lattice.thy	Sun Sep 13 22:56:52 2015 +0200
     6.3 @@ -921,7 +921,7 @@
     6.4  lemma (in weak_partial_order) weak_total_orderI:
     6.5    assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
     6.6    shows "weak_total_order L"
     6.7 -  by default (rule total)
     6.8 +  by standard (rule total)
     6.9  
    6.10  text {* Total orders are lattices. *}
    6.11  
    6.12 @@ -985,7 +985,7 @@
    6.13      and inf_exists:
    6.14      "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
    6.15    shows "weak_complete_lattice L"
    6.16 -  by default (auto intro: sup_exists inf_exists)
    6.17 +  by standard (auto intro: sup_exists inf_exists)
    6.18  
    6.19  definition
    6.20    top :: "_ => 'a" ("\<top>\<index>")
    6.21 @@ -1133,14 +1133,14 @@
    6.22      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
    6.23  
    6.24  sublocale upper_semilattice < weak: weak_upper_semilattice
    6.25 -  by default (rule sup_of_two_exists)
    6.26 +  by standard (rule sup_of_two_exists)
    6.27  
    6.28  locale lower_semilattice = partial_order +
    6.29    assumes inf_of_two_exists:
    6.30      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
    6.31  
    6.32  sublocale lower_semilattice < weak: weak_lower_semilattice
    6.33 -  by default (rule inf_of_two_exists)
    6.34 +  by standard (rule inf_of_two_exists)
    6.35  
    6.36  locale lattice = upper_semilattice + lower_semilattice
    6.37  
    6.38 @@ -1191,19 +1191,19 @@
    6.39    assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
    6.40  
    6.41  sublocale total_order < weak: weak_total_order
    6.42 -  by default (rule total_order_total)
    6.43 +  by standard (rule total_order_total)
    6.44  
    6.45  text {* Introduction rule: the usual definition of total order *}
    6.46  
    6.47  lemma (in partial_order) total_orderI:
    6.48    assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
    6.49    shows "total_order L"
    6.50 -  by default (rule total)
    6.51 +  by standard (rule total)
    6.52  
    6.53  text {* Total orders are lattices. *}
    6.54  
    6.55  sublocale total_order < weak: lattice
    6.56 -  by default (auto intro: sup_of_two_exists inf_of_two_exists)
    6.57 +  by standard (auto intro: sup_of_two_exists inf_of_two_exists)
    6.58  
    6.59  
    6.60  text {* Complete lattices *}
    6.61 @@ -1215,7 +1215,7 @@
    6.62      "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
    6.63  
    6.64  sublocale complete_lattice < weak: weak_complete_lattice
    6.65 -  by default (auto intro: sup_exists inf_exists)
    6.66 +  by standard (auto intro: sup_exists inf_exists)
    6.67  
    6.68  text {* Introduction rule: the usual definition of complete lattice *}
    6.69  
    6.70 @@ -1225,7 +1225,7 @@
    6.71      and inf_exists:
    6.72      "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
    6.73    shows "complete_lattice L"
    6.74 -  by default (auto intro: sup_exists inf_exists)
    6.75 +  by standard (auto intro: sup_exists inf_exists)
    6.76  
    6.77  theorem (in partial_order) complete_lattice_criterion1:
    6.78    assumes top_exists: "EX g. greatest L g (carrier L)"
    6.79 @@ -1282,7 +1282,7 @@
    6.80    (is "complete_lattice ?L")
    6.81  proof (rule partial_order.complete_latticeI)
    6.82    show "partial_order ?L"
    6.83 -    by default auto
    6.84 +    by standard auto
    6.85  next
    6.86    fix B
    6.87    assume "B \<subseteq> carrier ?L"
     7.1 --- a/src/HOL/Algebra/RingHom.thy	Sun Sep 13 22:25:21 2015 +0200
     7.2 +++ b/src/HOL/Algebra/RingHom.thy	Sun Sep 13 22:56:52 2015 +0200
     7.3 @@ -17,7 +17,7 @@
     7.4      and hom_one [simp] = ring_hom_one [OF homh]
     7.5  
     7.6  sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
     7.7 -  by default (rule homh)
     7.8 +  by standard (rule homh)
     7.9  
    7.10  sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
    7.11  apply (rule abelian_group_homI)
     8.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sun Sep 13 22:25:21 2015 +0200
     8.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Sun Sep 13 22:56:52 2015 +0200
     8.3 @@ -1760,7 +1760,7 @@
     8.4      and deg_r_0: "deg R r = 0"
     8.5      shows "r = monom P (eval R R id a f) 0"
     8.6  proof -
     8.7 -  interpret UP_pre_univ_prop R R id P by default simp
     8.8 +  interpret UP_pre_univ_prop R R id P by standard simp
     8.9    have eval_ring_hom: "eval R R id a \<in> ring_hom P R"
    8.10      using eval_ring_hom [OF a] by simp
    8.11    have "eval R R id a f = eval R R id a ?gq \<oplus>\<^bsub>R\<^esub> eval R R id a r"
     9.1 --- a/src/HOL/BNF_Fixpoint_Base.thy	Sun Sep 13 22:25:21 2015 +0200
     9.2 +++ b/src/HOL/BNF_Fixpoint_Base.thy	Sun Sep 13 22:56:52 2015 +0200
     9.3 @@ -15,10 +15,10 @@
     9.4  begin
     9.5  
     9.6  lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
     9.7 -  by default simp_all
     9.8 +  by standard simp_all
     9.9  
    9.10  lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
    9.11 -  by default simp_all
    9.12 +  by standard simp_all
    9.13  
    9.14  lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
    9.15    by auto
    10.1 --- a/src/HOL/Basic_BNF_LFPs.thy	Sun Sep 13 22:25:21 2015 +0200
    10.2 +++ b/src/HOL/Basic_BNF_LFPs.thy	Sun Sep 13 22:56:52 2015 +0200
    10.3 @@ -30,7 +30,7 @@
    10.4  lemmas xtor_inject = xtor_rel[of "op ="]
    10.5  
    10.6  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"
    10.7 -  unfolding xtor_def vimage2p_def id_bnf_def by default
    10.8 +  unfolding xtor_def vimage2p_def id_bnf_def ..
    10.9  
   10.10  lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (id_bnf (Inl a)))"
   10.11    unfolding xtor_def id_bnf_def by (rule reflexive)
   10.12 @@ -60,10 +60,10 @@
   10.13    by (cases p) auto
   10.14  
   10.15  lemma ex_neg_all_pos: "((\<exists>x. P x) \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
   10.16 -  by default blast+
   10.17 +  by standard blast+
   10.18  
   10.19  lemma hypsubst_in_prems: "(\<And>x. y = x \<Longrightarrow> z = f x \<Longrightarrow> P) \<equiv> (z = f y \<Longrightarrow> P)"
   10.20 -  by default blast+
   10.21 +  by standard blast+
   10.22  
   10.23  lemma isl_map_sum:
   10.24    "isl (map_sum f g s) = isl s"
    11.1 --- a/src/HOL/Complete_Partial_Order.thy	Sun Sep 13 22:25:21 2015 +0200
    11.2 +++ b/src/HOL/Complete_Partial_Order.thy	Sun Sep 13 22:56:52 2015 +0200
    11.3 @@ -293,7 +293,7 @@
    11.4  end
    11.5  
    11.6  instance complete_lattice \<subseteq> ccpo
    11.7 -  by default (fast intro: Sup_upper Sup_least)+
    11.8 +  by standard (fast intro: Sup_upper Sup_least)+
    11.9  
   11.10  lemma lfp_eq_fixp:
   11.11    assumes f: "mono f" shows "lfp f = fixp f"
    12.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Sun Sep 13 22:25:21 2015 +0200
    12.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Sun Sep 13 22:56:52 2015 +0200
    12.3 @@ -371,7 +371,7 @@
    12.4  end
    12.5  
    12.6  instance complete_lattice \<subseteq> conditionally_complete_lattice
    12.7 -  by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
    12.8 +  by standard (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
    12.9  
   12.10  lemma cSup_eq:
   12.11    fixes a :: "'a :: {conditionally_complete_lattice, no_bot}"
    13.1 --- a/src/HOL/Enum.thy	Sun Sep 13 22:25:21 2015 +0200
    13.2 +++ b/src/HOL/Enum.thy	Sun Sep 13 22:56:52 2015 +0200
    13.3 @@ -446,9 +446,10 @@
    13.4    "enum_ex P = enum_ex (%x. enum_ex (%y. P (x, y)))"
    13.5  
    13.6   
    13.7 -instance by default
    13.8 -  (simp_all add: enum_prod_def distinct_product
    13.9 -    enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def)
   13.10 +instance
   13.11 +  by standard
   13.12 +    (simp_all add: enum_prod_def distinct_product
   13.13 +      enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def)
   13.14  
   13.15  end
   13.16  
    14.1 --- a/src/HOL/Finite_Set.thy	Sun Sep 13 22:25:21 2015 +0200
    14.2 +++ b/src/HOL/Finite_Set.thy	Sun Sep 13 22:56:52 2015 +0200
    14.3 @@ -573,7 +573,7 @@
    14.4  end
    14.5  
    14.6  instance prod :: (finite, finite) finite
    14.7 -  by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
    14.8 +  by standard (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite)
    14.9  
   14.10  lemma inj_graph: "inj (%f. {(x, y). y = f x})"
   14.11    by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff)
   14.12 @@ -593,16 +593,16 @@
   14.13  qed
   14.14  
   14.15  instance bool :: finite
   14.16 -  by default (simp add: UNIV_bool)
   14.17 +  by standard (simp add: UNIV_bool)
   14.18  
   14.19  instance set :: (finite) finite
   14.20 -  by default (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)
   14.21 +  by standard (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite)
   14.22  
   14.23  instance unit :: finite
   14.24 -  by default (simp add: UNIV_unit)
   14.25 +  by standard (simp add: UNIV_unit)
   14.26  
   14.27  instance sum :: (finite, finite) finite
   14.28 -  by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
   14.29 +  by standard (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
   14.30  
   14.31  
   14.32  subsection \<open>A basic fold functional for finite sets\<close>
   14.33 @@ -967,7 +967,7 @@
   14.34    "comp_fun_commute (\<lambda>x A'. if P x then Set.insert x A' else A')"
   14.35  proof - 
   14.36    interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
   14.37 -  show ?thesis by default (auto simp: fun_eq_iff)
   14.38 +  show ?thesis by standard (auto simp: fun_eq_iff)
   14.39  qed
   14.40  
   14.41  lemma Set_filter_fold:
   14.42 @@ -988,7 +988,7 @@
   14.43    shows "image f A = fold (\<lambda>k A. Set.insert (f k) A) {} A"
   14.44  using assms
   14.45  proof -
   14.46 -  interpret comp_fun_commute "\<lambda>k A. Set.insert (f k) A" by default auto
   14.47 +  interpret comp_fun_commute "\<lambda>k A. Set.insert (f k) A" by standard auto
   14.48    show ?thesis using assms by (induct A) auto
   14.49  qed
   14.50  
   14.51 @@ -997,7 +997,7 @@
   14.52    shows "Ball A P = fold (\<lambda>k s. s \<and> P k) True A"
   14.53  using assms
   14.54  proof -
   14.55 -  interpret comp_fun_commute "\<lambda>k s. s \<and> P k" by default auto
   14.56 +  interpret comp_fun_commute "\<lambda>k s. s \<and> P k" by standard auto
   14.57    show ?thesis using assms by (induct A) auto
   14.58  qed
   14.59  
   14.60 @@ -1006,7 +1006,7 @@
   14.61    shows "Bex A P = fold (\<lambda>k s. s \<or> P k) False A"
   14.62  using assms
   14.63  proof -
   14.64 -  interpret comp_fun_commute "\<lambda>k s. s \<or> P k" by default auto
   14.65 +  interpret comp_fun_commute "\<lambda>k s. s \<or> P k" by standard auto
   14.66    show ?thesis using assms by (induct A) auto
   14.67  qed
   14.68  
   14.69 @@ -1027,14 +1027,14 @@
   14.70    assumes "finite B"
   14.71    shows "(\<Union>y\<in>B. {(x, y)}) \<union> A = fold (\<lambda>y. Set.insert (x, y)) A B"
   14.72  proof -
   14.73 -  interpret comp_fun_commute "\<lambda>y. Set.insert (x, y)" by default auto
   14.74 +  interpret comp_fun_commute "\<lambda>y. Set.insert (x, y)" by standard auto
   14.75    show ?thesis using assms  by (induct B arbitrary: A) simp_all
   14.76  qed
   14.77  
   14.78  lemma comp_fun_commute_product_fold: 
   14.79    assumes "finite B"
   14.80    shows "comp_fun_commute (\<lambda>x z. fold (\<lambda>y. Set.insert (x, y)) z B)" 
   14.81 -by default (auto simp: fold_union_pair[symmetric] assms)
   14.82 +  by standard (auto simp: fold_union_pair[symmetric] assms)
   14.83  
   14.84  lemma product_fold:
   14.85    assumes "finite A"
   14.86 @@ -1122,18 +1122,16 @@
   14.87  begin
   14.88  
   14.89  interpretation fold?: comp_fun_commute f
   14.90 -  by default (insert comp_fun_commute, simp add: fun_eq_iff)
   14.91 +  by standard (insert comp_fun_commute, simp add: fun_eq_iff)
   14.92  
   14.93  definition F :: "'a set \<Rightarrow> 'b"
   14.94  where
   14.95    eq_fold: "F A = fold f z A"
   14.96  
   14.97 -lemma empty [simp]:
   14.98 -  "F {} = z"
   14.99 +lemma empty [simp]:"F {} = z"
  14.100    by (simp add: eq_fold)
  14.101  
  14.102 -lemma infinite [simp]:
  14.103 -  "\<not> finite A \<Longrightarrow> F A = z"
  14.104 +lemma infinite [simp]: "\<not> finite A \<Longrightarrow> F A = z"
  14.105    by (simp add: eq_fold)
  14.106   
  14.107  lemma insert [simp]:
  14.108 @@ -1172,7 +1170,7 @@
  14.109  declare insert [simp del]
  14.110  
  14.111  interpretation fold?: comp_fun_idem f
  14.112 -  by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
  14.113 +  by standard (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff)
  14.114  
  14.115  lemma insert_idem [simp]:
  14.116    assumes "finite A"
  14.117 @@ -1202,7 +1200,7 @@
  14.118  where
  14.119    "folding.F (\<lambda>_. Suc) 0 = card"
  14.120  proof -
  14.121 -  show "folding (\<lambda>_. Suc)" by default rule
  14.122 +  show "folding (\<lambda>_. Suc)" by standard rule
  14.123    then interpret card!: folding "\<lambda>_. Suc" 0 .
  14.124    from card_def show "folding.F (\<lambda>_. Suc) 0 = card" by rule
  14.125  qed
    15.1 --- a/src/HOL/GCD.thy	Sun Sep 13 22:25:21 2015 +0200
    15.2 +++ b/src/HOL/GCD.thy	Sun Sep 13 22:56:52 2015 +0200
    15.3 @@ -1975,7 +1975,7 @@
    15.4    and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
    15.5  proof -
    15.6    show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
    15.7 -    by default (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
    15.8 +    by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
    15.9    then interpret gcd_lcm_complete_lattice_nat:
   15.10      complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
   15.11    from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" .
    16.1 --- a/src/HOL/Groups.thy	Sun Sep 13 22:25:21 2015 +0200
    16.2 +++ b/src/HOL/Groups.thy	Sun Sep 13 22:56:52 2015 +0200
    16.3 @@ -71,7 +71,7 @@
    16.4  begin
    16.5  
    16.6  sublocale monoid
    16.7 -  by default (simp_all add: commute comm_neutral)
    16.8 +  by standard (simp_all add: commute comm_neutral)
    16.9  
   16.10  end
   16.11  
   16.12 @@ -132,7 +132,7 @@
   16.13  begin
   16.14  
   16.15  sublocale add!: semigroup plus
   16.16 -  by default (fact add_assoc)
   16.17 +  by standard (fact add_assoc)
   16.18  
   16.19  end
   16.20  
   16.21 @@ -143,7 +143,7 @@
   16.22  begin
   16.23  
   16.24  sublocale add!: abel_semigroup plus
   16.25 -  by default (fact add_commute)
   16.26 +  by standard (fact add_commute)
   16.27  
   16.28  declare add.left_commute [algebra_simps, field_simps]
   16.29  
   16.30 @@ -160,7 +160,7 @@
   16.31  begin
   16.32  
   16.33  sublocale mult!: semigroup times
   16.34 -  by default (fact mult_assoc)
   16.35 +  by standard (fact mult_assoc)
   16.36  
   16.37  end
   16.38  
   16.39 @@ -171,7 +171,7 @@
   16.40  begin
   16.41  
   16.42  sublocale mult!: abel_semigroup times
   16.43 -  by default (fact mult_commute)
   16.44 +  by standard (fact mult_commute)
   16.45  
   16.46  declare mult.left_commute [algebra_simps, field_simps]
   16.47  
   16.48 @@ -189,7 +189,7 @@
   16.49  begin
   16.50  
   16.51  sublocale add!: monoid plus 0
   16.52 -  by default (fact add_0_left add_0_right)+
   16.53 +  by standard (fact add_0_left add_0_right)+
   16.54  
   16.55  end
   16.56  
   16.57 @@ -201,10 +201,10 @@
   16.58  begin
   16.59  
   16.60  subclass monoid_add
   16.61 -  by default (simp_all add: add_0 add.commute [of _ 0])
   16.62 +  by standard (simp_all add: add_0 add.commute [of _ 0])
   16.63  
   16.64  sublocale add!: comm_monoid plus 0
   16.65 -  by default (simp add: ac_simps)
   16.66 +  by standard (simp add: ac_simps)
   16.67  
   16.68  end
   16.69  
   16.70 @@ -214,7 +214,7 @@
   16.71  begin
   16.72  
   16.73  sublocale mult!: monoid times 1
   16.74 -  by default (fact mult_1_left mult_1_right)+
   16.75 +  by standard (fact mult_1_left mult_1_right)+
   16.76  
   16.77  end
   16.78  
   16.79 @@ -226,10 +226,10 @@
   16.80  begin
   16.81  
   16.82  subclass monoid_mult
   16.83 -  by default (simp_all add: mult_1 mult.commute [of _ 1])
   16.84 +  by standard (simp_all add: mult_1 mult.commute [of _ 1])
   16.85  
   16.86  sublocale mult!: comm_monoid times 1
   16.87 -  by default (simp add: ac_simps)
   16.88 +  by standard (simp add: ac_simps)
   16.89  
   16.90  end
   16.91  
    17.1 --- a/src/HOL/Groups_Big.thy	Sun Sep 13 22:25:21 2015 +0200
    17.2 +++ b/src/HOL/Groups_Big.thy	Sun Sep 13 22:56:52 2015 +0200
    17.3 @@ -18,7 +18,7 @@
    17.4  begin
    17.5  
    17.6  interpretation comp_fun_commute f
    17.7 -  by default (simp add: fun_eq_iff left_commute)
    17.8 +  by standard (simp add: fun_eq_iff left_commute)
    17.9  
   17.10  interpretation comp?: comp_fun_commute "f \<circ> g"
   17.11    by (fact comp_comp_fun_commute)
    18.1 --- a/src/HOL/HOL.thy	Sun Sep 13 22:25:21 2015 +0200
    18.2 +++ b/src/HOL/HOL.thy	Sun Sep 13 22:56:52 2015 +0200
    18.3 @@ -1254,10 +1254,10 @@
    18.4  qed
    18.5  
    18.6  lemma implies_True_equals: "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True"
    18.7 -by default (intro TrueI)
    18.8 +  by standard (intro TrueI)
    18.9  
   18.10  lemma False_implies_equals: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
   18.11 -by default simp_all
   18.12 +  by standard simp_all
   18.13  
   18.14  (* This is not made a simp rule because it does not improve any proofs
   18.15     but slows some AFP entries down by 5% (cpu time). May 2015 *)
    19.1 --- a/src/HOL/HOLCF/Bifinite.thy	Sun Sep 13 22:25:21 2015 +0200
    19.2 +++ b/src/HOL/HOLCF/Bifinite.thy	Sun Sep 13 22:56:52 2015 +0200
    19.3 @@ -162,7 +162,7 @@
    19.4  qed
    19.5  
    19.6  instance u :: (profinite) bifinite
    19.7 -  by default (rule profinite)
    19.8 +  by standard (rule profinite)
    19.9  
   19.10  text {*
   19.11    Types @{typ "'a \<rightarrow> 'b"} and @{typ "'a u \<rightarrow>! 'b"} are isomorphic.
   19.12 @@ -256,10 +256,10 @@
   19.13  by (simp add: approx_chain_def cfun_eq_iff finite_deflation_bottom)
   19.14  
   19.15  instance unit :: bifinite
   19.16 -  by default (fast intro!: approx_chain_unit)
   19.17 +  by standard (fast intro!: approx_chain_unit)
   19.18  
   19.19  instance discr :: (countable) profinite
   19.20 -  by default (fast intro!: discr_approx)
   19.21 +  by standard (fast intro!: discr_approx)
   19.22  
   19.23  instance lift :: (countable) bifinite
   19.24  proof
    20.1 --- a/src/HOL/HOLCF/Completion.thy	Sun Sep 13 22:25:21 2015 +0200
    20.2 +++ b/src/HOL/HOLCF/Completion.thy	Sun Sep 13 22:56:52 2015 +0200
    20.3 @@ -116,7 +116,7 @@
    20.4    assumes type: "type_definition Rep Abs {S. ideal S}"
    20.5    assumes below: "\<And>x y. x \<sqsubseteq> y \<longleftrightarrow> Rep x \<subseteq> Rep y"
    20.6    shows "OFCLASS('b, cpo_class)"
    20.7 -by (default, rule exI, erule typedef_ideal_lub [OF type below])
    20.8 +  by standard (rule exI, erule typedef_ideal_lub [OF type below])
    20.9  
   20.10  end
   20.11  
    21.1 --- a/src/HOL/HOLCF/ConvexPD.thy	Sun Sep 13 22:25:21 2015 +0200
    21.2 +++ b/src/HOL/HOLCF/ConvexPD.thy	Sun Sep 13 22:56:52 2015 +0200
    21.3 @@ -414,14 +414,14 @@
    21.4  by (simp add: convex_map_def convex_bind_bind)
    21.5  
    21.6  lemma ep_pair_convex_map: "ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)"
    21.7 -apply default
    21.8 +apply standard
    21.9  apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse)
   21.10  apply (induct_tac y rule: convex_pd_induct)
   21.11  apply (simp_all add: ep_pair.e_p_below monofun_cfun)
   21.12  done
   21.13  
   21.14  lemma deflation_convex_map: "deflation d \<Longrightarrow> deflation (convex_map\<cdot>d)"
   21.15 -apply default
   21.16 +apply standard
   21.17  apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem)
   21.18  apply (induct_tac x rule: convex_pd_induct)
   21.19  apply (simp_all add: deflation.below monofun_cfun)
    22.1 --- a/src/HOL/HOLCF/Deflation.thy	Sun Sep 13 22:25:21 2015 +0200
    22.2 +++ b/src/HOL/HOLCF/Deflation.thy	Sun Sep 13 22:56:52 2015 +0200
    22.3 @@ -161,7 +161,7 @@
    22.4  unfolding finite_deflation_def by simp
    22.5  
    22.6  lemma finite_deflation_bottom: "finite_deflation \<bottom>"
    22.7 -by default simp_all
    22.8 +by standard simp_all
    22.9  
   22.10  
   22.11  subsection {* Continuous embedding-projection pairs *}
   22.12 @@ -358,7 +358,7 @@
   22.13  subsection {* Composing ep-pairs *}
   22.14  
   22.15  lemma ep_pair_ID_ID: "ep_pair ID ID"
   22.16 -by default simp_all
   22.17 +by standard simp_all
   22.18  
   22.19  lemma ep_pair_comp:
   22.20    assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    23.1 --- a/src/HOL/HOLCF/Discrete.thy	Sun Sep 13 22:25:21 2015 +0200
    23.2 +++ b/src/HOL/HOLCF/Discrete.thy	Sun Sep 13 22:56:52 2015 +0200
    23.3 @@ -19,7 +19,7 @@
    23.4    "(op \<sqsubseteq> :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (op =)"
    23.5  
    23.6  instance
    23.7 -by default (simp add: below_discr_def)
    23.8 +  by standard (simp add: below_discr_def)
    23.9  
   23.10  end
   23.11  
    24.1 --- a/src/HOL/HOLCF/Domain.thy	Sun Sep 13 22:25:21 2015 +0200
    24.2 +++ b/src/HOL/HOLCF/Domain.thy	Sun Sep 13 22:56:52 2015 +0200
    24.3 @@ -125,7 +125,7 @@
    24.4      unfolding prj_beta emb_beta
    24.5      by (simp add: type_definition.Abs_inverse [OF type])
    24.6    show "ep_pair (emb :: 'a \<rightarrow> udom) prj"
    24.7 -    apply default
    24.8 +    apply standard
    24.9      apply (simp add: prj_emb)
   24.10      apply (simp add: emb_prj cast.below)
   24.11      done
    25.1 --- a/src/HOL/HOLCF/Fun_Cpo.thy	Sun Sep 13 22:25:21 2015 +0200
    25.2 +++ b/src/HOL/HOLCF/Fun_Cpo.thy	Sun Sep 13 22:56:52 2015 +0200
    25.3 @@ -93,7 +93,7 @@
    25.4  by (simp add: below_fun_def)
    25.5  
    25.6  instance "fun"  :: (type, pcpo) pcpo
    25.7 -by default (fast intro: minimal_fun)
    25.8 +by standard (fast intro: minimal_fun)
    25.9  
   25.10  lemma inst_fun_pcpo: "\<bottom> = (\<lambda>x. \<bottom>)"
   25.11  by (rule minimal_fun [THEN bottomI, symmetric])
    26.1 --- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Sep 13 22:25:21 2015 +0200
    26.2 +++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Sep 13 22:56:52 2015 +0200
    26.3 @@ -490,7 +490,7 @@
    26.4  by (fast intro: below_antisym meet_defl_below2 meet_defl_greatest)
    26.5  
    26.6  interpretation meet_defl: semilattice "\<lambda>a b. meet_defl\<cdot>a\<cdot>b"
    26.7 -by default
    26.8 +by standard
    26.9    (fast intro: below_antisym meet_defl_greatest
   26.10     meet_defl_below1 [THEN below_trans] meet_defl_below2 [THEN below_trans])+
   26.11  
    27.1 --- a/src/HOL/HOLCF/Library/List_Predomain.thy	Sun Sep 13 22:25:21 2015 +0200
    27.2 +++ b/src/HOL/HOLCF/Library/List_Predomain.thy	Sun Sep 13 22:56:52 2015 +0200
    27.3 @@ -143,7 +143,7 @@
    27.4  
    27.5  lemma deflation_list_map [domain_deflation]:
    27.6    "deflation d \<Longrightarrow> deflation (list_map d)"
    27.7 -apply default
    27.8 +apply standard
    27.9  apply (induct_tac x, simp_all add: deflation.idem)
   27.10  apply (induct_tac x, simp_all add: deflation.below)
   27.11  done
    28.1 --- a/src/HOL/HOLCF/Library/Option_Cpo.thy	Sun Sep 13 22:25:21 2015 +0200
    28.2 +++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Sun Sep 13 22:56:52 2015 +0200
    28.3 @@ -269,7 +269,7 @@
    28.4  
    28.5  lemma deflation_option_map [domain_deflation]:
    28.6    "deflation d \<Longrightarrow> deflation (option_map d)"
    28.7 -apply default
    28.8 +apply standard
    28.9  apply (induct_tac x, simp_all add: deflation.idem)
   28.10  apply (induct_tac x, simp_all add: deflation.below)
   28.11  done
    29.1 --- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Sun Sep 13 22:25:21 2015 +0200
    29.2 +++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Sun Sep 13 22:56:52 2015 +0200
    29.3 @@ -342,7 +342,7 @@
    29.4  
    29.5  lemma deflation_map_sum [domain_deflation]:
    29.6    "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (map_sum' d1 d2)"
    29.7 -apply default
    29.8 +apply standard
    29.9  apply (induct_tac x, simp_all add: deflation.idem)
   29.10  apply (induct_tac x, simp_all add: deflation.below)
   29.11  done
    30.1 --- a/src/HOL/HOLCF/LowerPD.thy	Sun Sep 13 22:25:21 2015 +0200
    30.2 +++ b/src/HOL/HOLCF/LowerPD.thy	Sun Sep 13 22:56:52 2015 +0200
    30.3 @@ -407,14 +407,14 @@
    30.4  by (simp add: lower_map_def lower_bind_bind)
    30.5  
    30.6  lemma ep_pair_lower_map: "ep_pair e p \<Longrightarrow> ep_pair (lower_map\<cdot>e) (lower_map\<cdot>p)"
    30.7 -apply default
    30.8 +apply standard
    30.9  apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse)
   30.10  apply (induct_tac y rule: lower_pd_induct)
   30.11  apply (simp_all add: ep_pair.e_p_below monofun_cfun del: lower_plus_below_iff)
   30.12  done
   30.13  
   30.14  lemma deflation_lower_map: "deflation d \<Longrightarrow> deflation (lower_map\<cdot>d)"
   30.15 -apply default
   30.16 +apply standard
   30.17  apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem)
   30.18  apply (induct_tac x rule: lower_pd_induct)
   30.19  apply (simp_all add: deflation.below monofun_cfun del: lower_plus_below_iff)
    31.1 --- a/src/HOL/HOLCF/Map_Functions.thy	Sun Sep 13 22:25:21 2015 +0200
    31.2 +++ b/src/HOL/HOLCF/Map_Functions.thy	Sun Sep 13 22:56:52 2015 +0200
    31.3 @@ -195,13 +195,13 @@
    31.4  by (simp add: cfcomp1 u_map_map eta_cfun)
    31.5  
    31.6  lemma ep_pair_u_map: "ep_pair e p \<Longrightarrow> ep_pair (u_map\<cdot>e) (u_map\<cdot>p)"
    31.7 -apply default
    31.8 +apply standard
    31.9  apply (case_tac x, simp, simp add: ep_pair.e_inverse)
   31.10  apply (case_tac y, simp, simp add: ep_pair.e_p_below)
   31.11  done
   31.12  
   31.13  lemma deflation_u_map: "deflation d \<Longrightarrow> deflation (u_map\<cdot>d)"
   31.14 -apply default
   31.15 +apply standard
   31.16  apply (case_tac x, simp, simp add: deflation.idem)
   31.17  apply (case_tac x, simp, simp add: deflation.below)
   31.18  done
    32.1 --- a/src/HOL/HOLCF/Pcpo.thy	Sun Sep 13 22:25:21 2015 +0200
    32.2 +++ b/src/HOL/HOLCF/Pcpo.thy	Sun Sep 13 22:56:52 2015 +0200
    32.3 @@ -198,7 +198,7 @@
    32.4  begin
    32.5  
    32.6  subclass cpo
    32.7 -apply default
    32.8 +apply standard
    32.9  apply (frule chfin)
   32.10  apply (blast intro: lub_finch1)
   32.11  done
   32.12 @@ -213,7 +213,7 @@
   32.13  begin
   32.14  
   32.15  subclass chfin
   32.16 -apply default
   32.17 +apply standard
   32.18  apply (unfold max_in_chain_def)
   32.19  apply (case_tac "\<forall>i. Y i = \<bottom>")
   32.20  apply simp
    33.1 --- a/src/HOL/HOLCF/Representable.thy	Sun Sep 13 22:25:21 2015 +0200
    33.2 +++ b/src/HOL/HOLCF/Representable.thy	Sun Sep 13 22:56:52 2015 +0200
    33.3 @@ -119,10 +119,10 @@
    33.4  qed
    33.5  
    33.6  instance "domain" \<subseteq> bifinite
    33.7 -by default (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL])
    33.8 +by standard (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL])
    33.9  
   33.10  instance predomain \<subseteq> profinite
   33.11 -by default (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
   33.12 +by standard (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl])
   33.13  
   33.14  subsection {* Universal domain ep-pairs *}
   33.15  
    34.1 --- a/src/HOL/HOLCF/Universal.thy	Sun Sep 13 22:25:21 2015 +0200
    34.2 +++ b/src/HOL/HOLCF/Universal.thy	Sun Sep 13 22:56:52 2015 +0200
    34.3 @@ -98,7 +98,7 @@
    34.4  done
    34.5  
    34.6  interpretation udom: preorder ubasis_le
    34.7 -apply default
    34.8 +apply standard
    34.9  apply (rule ubasis_le_refl)
   34.10  apply (erule (1) ubasis_le_trans)
   34.11  done
   34.12 @@ -879,7 +879,7 @@
   34.13  done
   34.14  
   34.15  lemma ep_pair_udom: "ep_pair udom_emb udom_prj"
   34.16 - apply default
   34.17 + apply standard
   34.18    apply (rule compact_basis.principal_induct, simp)
   34.19    apply (simp add: udom_emb_principal udom_prj_principal)
   34.20    apply (simp add: basis_prj_basis_emb)
   34.21 @@ -986,7 +986,7 @@
   34.22  qed
   34.23  
   34.24  instance udom :: bifinite
   34.25 -  by default (fast intro: udom_approx)
   34.26 +  by standard (fast intro: udom_approx)
   34.27  
   34.28  hide_const (open) node
   34.29  
    35.1 --- a/src/HOL/HOLCF/UpperPD.thy	Sun Sep 13 22:25:21 2015 +0200
    35.2 +++ b/src/HOL/HOLCF/UpperPD.thy	Sun Sep 13 22:56:52 2015 +0200
    35.3 @@ -400,14 +400,14 @@
    35.4  by (simp add: upper_map_def upper_bind_bind)
    35.5  
    35.6  lemma ep_pair_upper_map: "ep_pair e p \<Longrightarrow> ep_pair (upper_map\<cdot>e) (upper_map\<cdot>p)"
    35.7 -apply default
    35.8 +apply standard
    35.9  apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse)
   35.10  apply (induct_tac y rule: upper_pd_induct)
   35.11  apply (simp_all add: ep_pair.e_p_below monofun_cfun del: upper_below_plus_iff)
   35.12  done
   35.13  
   35.14  lemma deflation_upper_map: "deflation d \<Longrightarrow> deflation (upper_map\<cdot>d)"
   35.15 -apply default
   35.16 +apply standard
   35.17  apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem)
   35.18  apply (induct_tac x rule: upper_pd_induct)
   35.19  apply (simp_all add: deflation.below monofun_cfun del: upper_below_plus_iff)
    36.1 --- a/src/HOL/Int.thy	Sun Sep 13 22:25:21 2015 +0200
    36.2 +++ b/src/HOL/Int.thy	Sun Sep 13 22:56:52 2015 +0200
    36.3 @@ -66,7 +66,7 @@
    36.4  qed
    36.5  
    36.6  instance
    36.7 -  by default (transfer, clarsimp simp: algebra_simps)+
    36.8 +  by standard (transfer, clarsimp simp: algebra_simps)+
    36.9  
   36.10  end
   36.11  
   36.12 @@ -99,7 +99,7 @@
   36.13    by auto
   36.14  
   36.15  instance
   36.16 -  by default (transfer, force)+
   36.17 +  by standard (transfer, force)+
   36.18  
   36.19  end
   36.20  
   36.21 @@ -305,13 +305,13 @@
   36.22  
   36.23  
   36.24  instance int :: no_top
   36.25 -  apply default
   36.26 +  apply standard
   36.27    apply (rule_tac x="x + 1" in exI)
   36.28    apply simp
   36.29    done
   36.30  
   36.31  instance int :: no_bot
   36.32 -  apply default
   36.33 +  apply standard
   36.34    apply (rule_tac x="x - 1" in exI)
   36.35    apply simp
   36.36    done
   36.37 @@ -1526,7 +1526,8 @@
   36.38  definition
   36.39    "HOL.equal k l \<longleftrightarrow> k = (l::int)"
   36.40  
   36.41 -instance by default (rule equal_int_def)
   36.42 +instance
   36.43 +  by standard (rule equal_int_def)
   36.44  
   36.45  end
   36.46  
    37.1 --- a/src/HOL/Lattices.thy	Sun Sep 13 22:25:21 2015 +0200
    37.2 +++ b/src/HOL/Lattices.thy	Sun Sep 13 22:56:52 2015 +0200
    37.3 @@ -145,7 +145,7 @@
    37.4  begin
    37.5  
    37.6  sublocale ordering_top less_eq less 1
    37.7 -  by default (simp add: order_iff)
    37.8 +  by standard (simp add: order_iff)
    37.9  
   37.10  end
   37.11  
   37.12 @@ -283,7 +283,7 @@
   37.13  qed
   37.14  
   37.15  sublocale inf!: semilattice_order inf less_eq less
   37.16 -  by default (auto simp add: le_iff_inf less_le)
   37.17 +  by standard (auto simp add: le_iff_inf less_le)
   37.18  
   37.19  lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   37.20    by (fact inf.assoc)
   37.21 @@ -328,7 +328,7 @@
   37.22  qed
   37.23  
   37.24  sublocale sup!: semilattice_order sup greater_eq greater
   37.25 -  by default (auto simp add: le_iff_sup sup.commute less_le)
   37.26 +  by standard (auto simp add: le_iff_sup sup.commute less_le)
   37.27  
   37.28  lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   37.29    by (fact sup.assoc)
   37.30 @@ -717,7 +717,7 @@
   37.31  
   37.32  sublocale min!: semilattice_order min less_eq less
   37.33    + max!: semilattice_order max greater_eq greater
   37.34 -  by default (auto simp add: min_def max_def)
   37.35 +  by standard (auto simp add: min_def max_def)
   37.36  
   37.37  lemma min_le_iff_disj:
   37.38    "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
    38.1 --- a/src/HOL/Lattices_Big.thy	Sun Sep 13 22:25:21 2015 +0200
    38.2 +++ b/src/HOL/Lattices_Big.thy	Sun Sep 13 22:56:52 2015 +0200
    38.3 @@ -21,7 +21,7 @@
    38.4  begin
    38.5  
    38.6  interpretation comp_fun_idem f
    38.7 -  by default (simp_all add: fun_eq_iff left_commute)
    38.8 +  by standard (simp_all add: fun_eq_iff left_commute)
    38.9  
   38.10  definition F :: "'a set \<Rightarrow> 'a"
   38.11  where
   38.12 @@ -33,7 +33,7 @@
   38.13  proof (rule sym)
   38.14    let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
   38.15    interpret comp_fun_idem "?f"
   38.16 -    by default (simp_all add: fun_eq_iff commute left_commute split: option.split)
   38.17 +    by standard (simp_all add: fun_eq_iff commute left_commute split: option.split)
   38.18    from assms show "Finite_Set.fold f x A = F (insert x A)"
   38.19    proof induct
   38.20      case empty then show ?case by (simp add: eq_fold')
   38.21 @@ -189,7 +189,7 @@
   38.22  begin
   38.23  
   38.24  interpretation comp_fun_idem f
   38.25 -  by default (simp_all add: fun_eq_iff left_commute)
   38.26 +  by standard (simp_all add: fun_eq_iff left_commute)
   38.27  
   38.28  definition F :: "'a set \<Rightarrow> 'a"
   38.29  where
   38.30 @@ -496,9 +496,9 @@
   38.31    "semilattice_set.F min = Min"
   38.32    and "semilattice_set.F max = Max"
   38.33  proof -
   38.34 -  show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
   38.35 +  show "semilattice_order_set min less_eq less" by standard (auto simp add: min_def)
   38.36    then interpret Min!: semilattice_order_set min less_eq less .
   38.37 -  show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
   38.38 +  show "semilattice_order_set max greater_eq greater" by standard (auto simp add: max_def)
   38.39    then interpret Max!: semilattice_order_set max greater_eq greater .
   38.40    from Min_def show "semilattice_set.F min = Min" by rule
   38.41    from Max_def show "semilattice_set.F max = Max" by rule
    39.1 --- a/src/HOL/Limits.thy	Sun Sep 13 22:25:21 2015 +0200
    39.2 +++ b/src/HOL/Limits.thy	Sun Sep 13 22:56:52 2015 +0200
    39.3 @@ -710,13 +710,15 @@
    39.4  
    39.5  lemma (in bounded_bilinear) flip:
    39.6    "bounded_bilinear (\<lambda>x y. y ** x)"
    39.7 -  apply default
    39.8 +  apply standard
    39.9    apply (rule add_right)
   39.10    apply (rule add_left)
   39.11    apply (rule scaleR_right)
   39.12    apply (rule scaleR_left)
   39.13    apply (subst mult.commute)
   39.14 -  using bounded by fast
   39.15 +  using bounded
   39.16 +  apply fast
   39.17 +  done
   39.18  
   39.19  lemma (in bounded_bilinear) Bfun_prod_Zfun:
   39.20    assumes f: "Bfun f F"
    40.1 --- a/src/HOL/List.thy	Sun Sep 13 22:25:21 2015 +0200
    40.2 +++ b/src/HOL/List.thy	Sun Sep 13 22:56:52 2015 +0200
    40.3 @@ -2868,7 +2868,7 @@
    40.4    "F (set (x # xs)) = fold f xs x"
    40.5  proof -
    40.6    interpret comp_fun_idem f
    40.7 -    by default (simp_all add: fun_eq_iff left_commute)
    40.8 +    by standard (simp_all add: fun_eq_iff left_commute)
    40.9    show ?thesis by (simp add: eq_fold fold_set_fold)
   40.10  qed
   40.11  
   40.12 @@ -5161,7 +5161,7 @@
   40.13    "folding.F insort [] = sorted_list_of_set"
   40.14  proof -
   40.15    interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
   40.16 -  show "folding insort" by default (fact comp_fun_commute)
   40.17 +  show "folding insort" by standard (fact comp_fun_commute)
   40.18    show "folding.F insort [] = sorted_list_of_set" by (simp only: sorted_list_of_set_def)
   40.19  qed
   40.20  
    41.1 --- a/src/HOL/Matrix_LP/Matrix.thy	Sun Sep 13 22:25:21 2015 +0200
    41.2 +++ b/src/HOL/Matrix_LP/Matrix.thy	Sun Sep 13 22:56:52 2015 +0200
    41.3 @@ -1448,7 +1448,7 @@
    41.4  definition "sup = combine_matrix sup"
    41.5  
    41.6  instance
    41.7 -  by default (auto simp add: le_infI le_matrix_def inf_matrix_def sup_matrix_def)
    41.8 +  by standard (auto simp add: le_infI le_matrix_def inf_matrix_def sup_matrix_def)
    41.9  
   41.10  end
   41.11  
    42.1 --- a/src/HOL/Matrix_LP/SparseMatrix.thy	Sun Sep 13 22:25:21 2015 +0200
    42.2 +++ b/src/HOL/Matrix_LP/SparseMatrix.thy	Sun Sep 13 22:56:52 2015 +0200
    42.3 @@ -120,8 +120,11 @@
    42.4    done
    42.5  
    42.6  instance matrix :: (lattice_ab_group_add_abs) lattice_ab_group_add_abs
    42.7 -apply default
    42.8 -unfolding abs_matrix_def .. (*FIXME move*)
    42.9 +  apply standard
   42.10 +  unfolding abs_matrix_def
   42.11 +  apply rule
   42.12 +  done
   42.13 +  (*FIXME move*)
   42.14  
   42.15  lemma sparse_row_vector_abs:
   42.16    "sorted_spvec (v :: 'a::lattice_ring spvec) \<Longrightarrow> sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)"
    43.1 --- a/src/HOL/MicroJava/J/State.thy	Sun Sep 13 22:25:21 2015 +0200
    43.2 +++ b/src/HOL/MicroJava/J/State.thy	Sun Sep 13 22:56:52 2015 +0200
    43.3 @@ -191,7 +191,7 @@
    43.4  begin
    43.5  
    43.6  definition "HOL.equal (l :: loc') l' \<longleftrightarrow> l = l'"
    43.7 -instance by default (simp add: equal_loc'_def)
    43.8 +instance by standard (simp add: equal_loc'_def)
    43.9  
   43.10  end
   43.11  
    44.1 --- a/src/HOL/MicroJava/J/Type.thy	Sun Sep 13 22:25:21 2015 +0200
    44.2 +++ b/src/HOL/MicroJava/J/Type.thy	Sun Sep 13 22:56:52 2015 +0200
    44.3 @@ -13,7 +13,7 @@
    44.4  begin
    44.5  
    44.6  definition "HOL.equal (cn :: cnam) cn' \<longleftrightarrow> cn = cn'"
    44.7 -instance by default (simp add: equal_cnam_def)
    44.8 +instance by standard (simp add: equal_cnam_def)
    44.9  
   44.10  end
   44.11  
   44.12 @@ -63,7 +63,7 @@
   44.13  begin
   44.14  
   44.15  definition "HOL.equal (vn :: vnam) vn' \<longleftrightarrow> vn = vn'"
   44.16 -instance by default (simp add: equal_vnam_def)
   44.17 +instance by standard (simp add: equal_vnam_def)
   44.18  
   44.19  end
   44.20  
   44.21 @@ -98,7 +98,7 @@
   44.22  begin
   44.23  
   44.24  definition "HOL.equal (M :: mname) M' \<longleftrightarrow> M = M'"
   44.25 -instance by default (simp add: equal_mname_def)
   44.26 +instance by standard (simp add: equal_mname_def)
   44.27  
   44.28  end
   44.29  
    45.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Sun Sep 13 22:25:21 2015 +0200
    45.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Sun Sep 13 22:56:52 2015 +0200
    45.3 @@ -315,7 +315,7 @@
    45.4    by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun)
    45.5  
    45.6  instance
    45.7 -  by default
    45.8 +  by standard
    45.9      (simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def
   45.10        Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps
   45.11        plus_cont const_bcontfun minus_cont scaleR_cont)
    46.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sun Sep 13 22:25:21 2015 +0200
    46.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sun Sep 13 22:56:52 2015 +0200
    46.3 @@ -589,7 +589,7 @@
    46.4        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>)
    46.5  
    46.6      show ?thesis
    46.7 -    proof (rule ksimplex.intros, default)
    46.8 +    proof (rule ksimplex.intros, standard)
    46.9        show "bij_betw (upd\<circ>Suc) {..< n} {..< n}" by fact
   46.10        show "base(n := p) \<in> {..<n} \<rightarrow> {..<p}" "\<And>i. n\<le>i \<Longrightarrow> (base(n := p)) i = p"
   46.11          using base base_out by (auto simp: Pi_iff)
   46.12 @@ -620,7 +620,7 @@
   46.13      def u \<equiv> "\<lambda>i. case i of 0 \<Rightarrow> n | Suc i \<Rightarrow> upd i"
   46.14  
   46.15      have "ksimplex p (Suc n) (s' \<union> {b})"
   46.16 -    proof (rule ksimplex.intros, default)
   46.17 +    proof (rule ksimplex.intros, standard)
   46.18        show "b \<in> {..<Suc n} \<rightarrow> {..<p}"
   46.19          using base \<open>0 < p\<close> unfolding lessThan_Suc b_def by (auto simp: PiE_iff)
   46.20        show "\<And>i. Suc n \<le> i \<Longrightarrow> b i = p"
    47.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Sep 13 22:25:21 2015 +0200
    47.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Sep 13 22:56:52 2015 +0200
    47.3 @@ -73,7 +73,7 @@
    47.4  end
    47.5  
    47.6  instance vec:: (order, finite) order
    47.7 -  by default (auto simp: less_eq_vec_def less_vec_def vec_eq_iff
    47.8 +  by standard (auto simp: less_eq_vec_def less_vec_def vec_eq_iff
    47.9        intro: order.trans order.antisym order.strict_implies_order)
   47.10  
   47.11  instance vec :: (linorder, cart_one) linorder
   47.12 @@ -183,26 +183,26 @@
   47.13  subsection \<open>Some frequently useful arithmetic lemmas over vectors.\<close>
   47.14  
   47.15  instance vec :: (semigroup_mult, finite) semigroup_mult
   47.16 -  by default (vector mult.assoc)
   47.17 +  by standard (vector mult.assoc)
   47.18  
   47.19  instance vec :: (monoid_mult, finite) monoid_mult
   47.20 -  by default vector+
   47.21 +  by standard vector+
   47.22  
   47.23  instance vec :: (ab_semigroup_mult, finite) ab_semigroup_mult
   47.24 -  by default (vector mult.commute)
   47.25 +  by standard (vector mult.commute)
   47.26  
   47.27  instance vec :: (comm_monoid_mult, finite) comm_monoid_mult
   47.28 -  by default vector
   47.29 +  by standard vector
   47.30  
   47.31  instance vec :: (semiring, finite) semiring
   47.32 -  by default (vector field_simps)+
   47.33 +  by standard (vector field_simps)+
   47.34  
   47.35  instance vec :: (semiring_0, finite) semiring_0
   47.36 -  by default (vector field_simps)+
   47.37 +  by standard (vector field_simps)+
   47.38  instance vec :: (semiring_1, finite) semiring_1
   47.39 -  by default vector
   47.40 +  by standard vector
   47.41  instance vec :: (comm_semiring, finite) comm_semiring
   47.42 -  by default (vector field_simps)+
   47.43 +  by standard (vector field_simps)+
   47.44  
   47.45  instance vec :: (comm_semiring_0, finite) comm_semiring_0 ..
   47.46  instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
   47.47 @@ -215,7 +215,7 @@
   47.48  instance vec :: (ring_1, finite) ring_1 ..
   47.49  
   47.50  instance vec :: (real_algebra, finite) real_algebra
   47.51 -  by default (simp_all add: vec_eq_iff)
   47.52 +  by standard (simp_all add: vec_eq_iff)
   47.53  
   47.54  instance vec :: (real_algebra_1, finite) real_algebra_1 ..
   47.55  
    48.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Sep 13 22:25:21 2015 +0200
    48.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Sep 13 22:56:52 2015 +0200
    48.3 @@ -139,7 +139,7 @@
    48.4    [simp]: "Basis = {1::real}"
    48.5  
    48.6  instance
    48.7 -  by default auto
    48.8 +  by standard auto
    48.9  
   48.10  end
   48.11  
   48.12 @@ -155,7 +155,7 @@
   48.13    "Basis = {1, ii}"
   48.14  
   48.15  instance
   48.16 -  by default (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm)
   48.17 +  by standard (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm)
   48.18  
   48.19  end
   48.20  
    49.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Sep 13 22:25:21 2015 +0200
    49.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Sun Sep 13 22:56:52 2015 +0200
    49.3 @@ -53,7 +53,7 @@
    49.4  qed
    49.5  
    49.6  instance ereal :: second_countable_topology
    49.7 -proof (default, intro exI conjI)
    49.8 +proof (standard, intro exI conjI)
    49.9    let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"
   49.10    show "countable ?B"
   49.11      by (auto intro: countable_rat)
    50.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Sep 13 22:25:21 2015 +0200
    50.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Sun Sep 13 22:56:52 2015 +0200
    50.3 @@ -95,30 +95,30 @@
    50.4    unfolding uminus_vec_def by simp
    50.5  
    50.6  instance vec :: (semigroup_add, finite) semigroup_add
    50.7 -  by default (simp add: vec_eq_iff add.assoc)
    50.8 +  by standard (simp add: vec_eq_iff add.assoc)
    50.9  
   50.10  instance vec :: (ab_semigroup_add, finite) ab_semigroup_add
   50.11 -  by default (simp add: vec_eq_iff add.commute)
   50.12 +  by standard (simp add: vec_eq_iff add.commute)
   50.13  
   50.14  instance vec :: (monoid_add, finite) monoid_add
   50.15 -  by default (simp_all add: vec_eq_iff)
   50.16 +  by standard (simp_all add: vec_eq_iff)
   50.17  
   50.18  instance vec :: (comm_monoid_add, finite) comm_monoid_add
   50.19 -  by default (simp add: vec_eq_iff)
   50.20 +  by standard (simp add: vec_eq_iff)
   50.21  
   50.22  instance vec :: (cancel_semigroup_add, finite) cancel_semigroup_add
   50.23 -  by default (simp_all add: vec_eq_iff)
   50.24 +  by standard (simp_all add: vec_eq_iff)
   50.25  
   50.26  instance vec :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add
   50.27 -  by default (simp_all add: vec_eq_iff diff_diff_eq)
   50.28 +  by standard (simp_all add: vec_eq_iff diff_diff_eq)
   50.29  
   50.30  instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
   50.31  
   50.32  instance vec :: (group_add, finite) group_add
   50.33 -  by default (simp_all add: vec_eq_iff)
   50.34 +  by standard (simp_all add: vec_eq_iff)
   50.35  
   50.36  instance vec :: (ab_group_add, finite) ab_group_add
   50.37 -  by default (simp_all add: vec_eq_iff)
   50.38 +  by standard (simp_all add: vec_eq_iff)
   50.39  
   50.40  
   50.41  subsection \<open>Real vector space\<close>
   50.42 @@ -132,7 +132,7 @@
   50.43    unfolding scaleR_vec_def by simp
   50.44  
   50.45  instance
   50.46 -  by default (simp_all add: vec_eq_iff scaleR_left_distrib scaleR_right_distrib)
   50.47 +  by standard (simp_all add: vec_eq_iff scaleR_left_distrib scaleR_right_distrib)
   50.48  
   50.49  end
   50.50  
   50.51 @@ -412,7 +412,7 @@
   50.52  by (rule member_le_setL2) simp_all
   50.53  
   50.54  lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
   50.55 -apply default
   50.56 +apply standard
   50.57  apply (rule vector_add_component)
   50.58  apply (rule vector_scaleR_component)
   50.59  apply (rule_tac x="1" in exI, simp add: norm_nth_le)
    51.1 --- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Sun Sep 13 22:25:21 2015 +0200
    51.2 +++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy	Sun Sep 13 22:56:52 2015 +0200
    51.3 @@ -17,20 +17,20 @@
    51.4  begin
    51.5  
    51.6  subclass order
    51.7 -  by default
    51.8 +  by standard
    51.9      (auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans)
   51.10  
   51.11  subclass ordered_ab_group_add_abs
   51.12 -  by default (auto simp: eucl_le inner_add_left eucl_abs abs_leI)
   51.13 +  by standard (auto simp: eucl_le inner_add_left eucl_abs abs_leI)
   51.14  
   51.15  subclass ordered_real_vector
   51.16 -  by default (auto simp: eucl_le intro!: mult_left_mono mult_right_mono)
   51.17 +  by standard (auto simp: eucl_le intro!: mult_left_mono mult_right_mono)
   51.18  
   51.19  subclass lattice
   51.20 -  by default (auto simp: eucl_inf eucl_sup eucl_le)
   51.21 +  by standard (auto simp: eucl_inf eucl_sup eucl_le)
   51.22  
   51.23  subclass distrib_lattice
   51.24 -  by default (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI)
   51.25 +  by standard (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI)
   51.26  
   51.27  subclass conditionally_complete_lattice
   51.28  proof
   51.29 @@ -152,7 +152,7 @@
   51.30    by (auto)
   51.31  
   51.32  instance real :: ordered_euclidean_space
   51.33 -  by default (auto simp: INF_def SUP_def)
   51.34 +  by standard (auto simp: INF_def SUP_def)
   51.35  
   51.36  lemma in_Basis_prod_iff:
   51.37    fixes i::"'a::euclidean_space*'b::euclidean_space"
   51.38 @@ -168,7 +168,7 @@
   51.39  end
   51.40  
   51.41  instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
   51.42 -  by default
   51.43 +  by standard
   51.44      (auto intro!: add_mono simp add: euclidean_representation_setsum'  Ball_def inner_prod_def
   51.45        in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def
   51.46        inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a]
   51.47 @@ -281,7 +281,7 @@
   51.48  definition "abs x = (\<chi> i. abs (x $ i))"
   51.49  
   51.50  instance
   51.51 -  apply default
   51.52 +  apply standard
   51.53    unfolding euclidean_representation_setsum'
   51.54    apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis
   51.55      Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left
    52.1 --- a/src/HOL/Nat.thy	Sun Sep 13 22:25:21 2015 +0200
    52.2 +++ b/src/HOL/Nat.thy	Sun Sep 13 22:56:52 2015 +0200
    52.3 @@ -529,7 +529,7 @@
    52.4  end
    52.5  
    52.6  instance nat :: no_top
    52.7 -  by default (auto intro: less_Suc_eq_le [THEN iffD2])
    52.8 +  by standard (auto intro: less_Suc_eq_le [THEN iffD2])
    52.9  
   52.10  
   52.11  subsubsection \<open>Introduction properties\<close>
    53.1 --- a/src/HOL/Nominal/Examples/Pattern.thy	Sun Sep 13 22:25:21 2015 +0200
    53.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Sun Sep 13 22:56:52 2015 +0200
    53.3 @@ -62,7 +62,7 @@
    53.4    by (simp add: supp_def Collect_disj_eq del: disj_not1)
    53.5  
    53.6  instance pat :: pt_name
    53.7 -proof (default, goal_cases)
    53.8 +proof (standard, goal_cases)
    53.9    case (1 x)
   53.10    show ?case by (induct x) simp_all
   53.11  next
   53.12 @@ -74,7 +74,7 @@
   53.13  qed
   53.14  
   53.15  instance pat :: fs_name
   53.16 -proof (default, goal_cases)
   53.17 +proof (standard, goal_cases)
   53.18    case (1 x)
   53.19    show ?case by (induct x) (simp_all add: fin_supp)
   53.20  qed
    54.1 --- a/src/HOL/Num.thy	Sun Sep 13 22:25:21 2015 +0200
    54.2 +++ b/src/HOL/Num.thy	Sun Sep 13 22:56:52 2015 +0200
    54.3 @@ -106,7 +106,7 @@
    54.4    "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
    54.5  
    54.6  instance
    54.7 -  by (default, auto simp add: less_num_def less_eq_num_def num_eq_iff)
    54.8 +  by standard (auto simp add: less_num_def less_eq_num_def num_eq_iff)
    54.9  
   54.10  end
   54.11  
    55.1 --- a/src/HOL/Orderings.thy	Sun Sep 13 22:25:21 2015 +0200
    55.2 +++ b/src/HOL/Orderings.thy	Sun Sep 13 22:56:52 2015 +0200
    55.3 @@ -196,7 +196,7 @@
    55.4    by (auto simp add: less_le_not_le intro: antisym)
    55.5  
    55.6  sublocale order!: ordering less_eq less +  dual_order!: ordering greater_eq greater
    55.7 -  by default (auto intro: antisym order_trans simp add: less_le)
    55.8 +  by standard (auto intro: antisym order_trans simp add: less_le)
    55.9  
   55.10  
   55.11  text \<open>Reflexivity.\<close>
   55.12 @@ -1197,7 +1197,7 @@
   55.13  begin
   55.14  
   55.15  sublocale bot!: ordering_top greater_eq greater bot
   55.16 -  by default (fact bot_least)
   55.17 +  by standard (fact bot_least)
   55.18  
   55.19  lemma le_bot:
   55.20    "a \<le> \<bottom> \<Longrightarrow> a = \<bottom>"
   55.21 @@ -1225,7 +1225,7 @@
   55.22  begin
   55.23  
   55.24  sublocale top!: ordering_top less_eq less top
   55.25 -  by default (fact top_greatest)
   55.26 +  by standard (fact top_greatest)
   55.27  
   55.28  lemma top_le:
   55.29    "\<top> \<le> a \<Longrightarrow> a = \<top>"
    56.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Sun Sep 13 22:25:21 2015 +0200
    56.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Sun Sep 13 22:56:52 2015 +0200
    56.3 @@ -702,7 +702,7 @@
    56.4  proof (rule measure_eqI)
    56.5    interpret A: finite_measure "count_space A" by (rule finite_measure_count_space) fact
    56.6    interpret B: finite_measure "count_space B" by (rule finite_measure_count_space) fact
    56.7 -  interpret P: pair_sigma_finite "count_space A" "count_space B" by default
    56.8 +  interpret P: pair_sigma_finite "count_space A" "count_space B" ..
    56.9    show eq: "sets ?P = sets ?C"
   56.10      by (simp add: sets_pair_measure sigma_sets_pair_measure_generator_finite A B)
   56.11    fix X assume X: "X \<in> sets ?P"
   56.12 @@ -890,7 +890,7 @@
   56.13  proof -
   56.14    interpret M1: sigma_finite_measure M1 by fact
   56.15    interpret M2: sigma_finite_measure M2 by fact
   56.16 -  interpret pair_sigma_finite M1 M2 by default
   56.17 +  interpret pair_sigma_finite M1 M2 ..
   56.18    from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
   56.19    let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
   56.20    let ?P = "M1 \<Otimes>\<^sub>M M2"
    57.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Sun Sep 13 22:25:21 2015 +0200
    57.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Sun Sep 13 22:56:52 2015 +0200
    57.3 @@ -2549,7 +2549,7 @@
    57.4    assumes "integrable (M1 \<Otimes>\<^sub>M M2) f"
    57.5    shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x))"
    57.6  proof -
    57.7 -  interpret Q: pair_sigma_finite M2 M1 by default
    57.8 +  interpret Q: pair_sigma_finite M2 M1 ..
    57.9    have *: "(\<lambda>(x,y). f (y,x)) = (\<lambda>x. f (case x of (x,y)\<Rightarrow>(y,x)))" by (auto simp: fun_eq_iff)
   57.10    show ?thesis unfolding *
   57.11      by (rule integrable_distr[OF measurable_pair_swap'])
   57.12 @@ -2560,7 +2560,7 @@
   57.13    fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
   57.14    shows "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x,y). f (y,x)) \<longleftrightarrow> integrable (M1 \<Otimes>\<^sub>M M2) f"
   57.15  proof -
   57.16 -  interpret Q: pair_sigma_finite M2 M1 by default
   57.17 +  interpret Q: pair_sigma_finite M2 M1 ..
   57.18    from Q.integrable_product_swap[of "\<lambda>(x,y). f (y,x)"] integrable_product_swap[of f]
   57.19    show ?thesis by auto
   57.20  qed
   57.21 @@ -2751,7 +2751,7 @@
   57.22      and integrable_snd: "integrable M2 (\<lambda>y. \<integral>x. f x y \<partial>M1)" (is "?INT")
   57.23      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")
   57.24  proof -
   57.25 -  interpret Q: pair_sigma_finite M2 M1 by default
   57.26 +  interpret Q: pair_sigma_finite M2 M1 ..
   57.27    have Q_int: "integrable (M2 \<Otimes>\<^sub>M M1) (\<lambda>(x, y). f y x)"
   57.28      using f unfolding integrable_product_swap_iff[symmetric] by simp
   57.29    show ?AE  using Q.AE_integrable_fst'[OF Q_int] by simp
   57.30 @@ -2780,11 +2780,11 @@
   57.31    and f: "integrable (Pi\<^sub>M (I \<union> J) M) f"
   57.32    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)"
   57.33  proof -
   57.34 -  interpret I: finite_product_sigma_finite M I by default fact
   57.35 -  interpret J: finite_product_sigma_finite M J by default fact
   57.36 +  interpret I: finite_product_sigma_finite M I by standard fact
   57.37 +  interpret J: finite_product_sigma_finite M J by standard fact
   57.38    have "finite (I \<union> J)" using fin by auto
   57.39 -  interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
   57.40 -  interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default
   57.41 +  interpret IJ: finite_product_sigma_finite M "I \<union> J" by standard fact
   57.42 +  interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" ..
   57.43    let ?M = "merge I J"
   57.44    let ?f = "\<lambda>x. f (?M x)"
   57.45    from f have f_borel: "f \<in> borel_measurable (Pi\<^sub>M (I \<union> J) M)"
   57.46 @@ -2830,7 +2830,7 @@
   57.47    assumes [simp]: "finite I" and integrable: "\<And>i. i \<in> I \<Longrightarrow> integrable (M i) (f i)"
   57.48    shows "integrable (Pi\<^sub>M I M) (\<lambda>x. (\<Prod>i\<in>I. f i (x i)))" (is "integrable _ ?f")
   57.49  proof (unfold integrable_iff_bounded, intro conjI)
   57.50 -  interpret finite_product_sigma_finite M I by default fact
   57.51 +  interpret finite_product_sigma_finite M I by standard fact
   57.52  
   57.53    show "?f \<in> borel_measurable (Pi\<^sub>M I M)"
   57.54      using assms by simp
   57.55 @@ -2859,7 +2859,7 @@
   57.56    then have prod: "\<And>J. J \<subseteq> insert i I \<Longrightarrow>
   57.57      integrable (Pi\<^sub>M J M) (\<lambda>x. (\<Prod>i\<in>J. f i (x i)))"
   57.58      by (intro product_integrable_setprod insert(4)) (auto intro: finite_subset)
   57.59 -  interpret I: finite_product_sigma_finite M I by default fact
   57.60 +  interpret I: finite_product_sigma_finite M I by standard fact
   57.61    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))"
   57.62      using `i \<notin> I` by (auto intro!: setprod.cong)
   57.63    show ?case
    58.1 --- a/src/HOL/Probability/Embed_Measure.thy	Sun Sep 13 22:25:21 2015 +0200
    58.2 +++ b/src/HOL/Probability/Embed_Measure.thy	Sun Sep 13 22:56:52 2015 +0200
    58.3 @@ -169,7 +169,7 @@
    58.4    from A_props and inj have "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
    58.5      by (intro ballI, subst emeasure_embed_measure)
    58.6         (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
    58.7 -  ultimately show ?thesis by - (default, blast)
    58.8 +  ultimately show ?thesis by - (standard, blast)
    58.9  qed
   58.10  
   58.11  lemma embed_measure_count_space':
    59.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Sun Sep 13 22:25:21 2015 +0200
    59.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Sun Sep 13 22:56:52 2015 +0200
    59.3 @@ -764,9 +764,9 @@
    59.4    "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))"
    59.5  proof (induct I arbitrary: A rule: finite_induct)
    59.6    case (insert i I)
    59.7 -  interpret finite_product_sigma_finite M I by default fact
    59.8 +  interpret finite_product_sigma_finite M I by standard fact
    59.9    have "finite (insert i I)" using `finite I` by auto
   59.10 -  interpret I': finite_product_sigma_finite M "insert i I" by default fact
   59.11 +  interpret I': finite_product_sigma_finite M "insert i I" by standard fact
   59.12    let ?h = "(\<lambda>(f, y). f(i := y))"
   59.13  
   59.14    let ?P = "distr (Pi\<^sub>M I M \<Otimes>\<^sub>M M i) (Pi\<^sub>M (insert i I) M) ?h"
   59.15 @@ -821,7 +821,7 @@
   59.16    assumes "finite I"
   59.17    shows "sigma_finite_measure (PiM I M)"
   59.18  proof
   59.19 -  interpret finite_product_sigma_finite M I by default fact
   59.20 +  interpret finite_product_sigma_finite M I by standard fact
   59.21  
   59.22    obtain F where F: "\<And>j. countable (F j)" "\<And>j f. f \<in> F j \<Longrightarrow> f \<in> sets (M j)"
   59.23      "\<And>j f. f \<in> F j \<Longrightarrow> emeasure (M j) f \<noteq> \<infinity>" and
   59.24 @@ -846,7 +846,7 @@
   59.25    assumes pos: "0 \<le> f (\<lambda>k. undefined)"
   59.26    shows "integral\<^sup>N (Pi\<^sub>M {} M) f = f (\<lambda>k. undefined)"
   59.27  proof -
   59.28 -  interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI)
   59.29 +  interpret finite_product_sigma_finite M "{}" by standard (fact finite.emptyI)
   59.30    have "\<And>A. emeasure (Pi\<^sub>M {} M) (Pi\<^sub>E {} A) = 1"
   59.31      using assms by (subst measure_times) auto
   59.32    then show ?thesis
   59.33 @@ -864,11 +864,11 @@
   59.34    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"
   59.35     (is "?D = ?P")
   59.36  proof -
   59.37 -  interpret I: finite_product_sigma_finite M I by default fact
   59.38 -  interpret J: finite_product_sigma_finite M J by default fact
   59.39 +  interpret I: finite_product_sigma_finite M I by standard fact
   59.40 +  interpret J: finite_product_sigma_finite M J by standard fact
   59.41    have "finite (I \<union> J)" using fin by auto
   59.42 -  interpret IJ: finite_product_sigma_finite M "I \<union> J" by default fact
   59.43 -  interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default
   59.44 +  interpret IJ: finite_product_sigma_finite M "I \<union> J" by standard fact
   59.45 +  interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard
   59.46    let ?g = "merge I J"
   59.47  
   59.48    from IJ.sigma_finite_pairs obtain F where
   59.49 @@ -928,9 +928,9 @@
   59.50    shows "integral\<^sup>N (Pi\<^sub>M (I \<union> J) M) f =
   59.51      (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. f (merge I J (x, y)) \<partial>(Pi\<^sub>M J M)) \<partial>(Pi\<^sub>M I M))"
   59.52  proof -
   59.53 -  interpret I: finite_product_sigma_finite M I by default fact
   59.54 -  interpret J: finite_product_sigma_finite M J by default fact
   59.55 -  interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default
   59.56 +  interpret I: finite_product_sigma_finite M I by standard fact
   59.57 +  interpret J: finite_product_sigma_finite M J by standard fact
   59.58 +  interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard
   59.59    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)"
   59.60      using measurable_comp[OF measurable_merge f] by (simp add: comp_def)
   59.61    show ?thesis
   59.62 @@ -944,7 +944,7 @@
   59.63  lemma (in product_sigma_finite) distr_singleton:
   59.64    "distr (Pi\<^sub>M {i} M) (M i) (\<lambda>x. x i) = M i" (is "?D = _")
   59.65  proof (intro measure_eqI[symmetric])
   59.66 -  interpret I: finite_product_sigma_finite M "{i}" by default simp
   59.67 +  interpret I: finite_product_sigma_finite M "{i}" by standard simp
   59.68    fix A assume A: "A \<in> sets (M i)"
   59.69    then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M {i} M) = (\<Pi>\<^sub>E i\<in>{i}. A)"
   59.70      using sets.sets_into_space by (auto simp: space_PiM)
   59.71 @@ -957,7 +957,7 @@
   59.72    assumes f: "f \<in> borel_measurable (M i)"
   59.73    shows "integral\<^sup>N (Pi\<^sub>M {i} M) (\<lambda>x. f (x i)) = integral\<^sup>N (M i) f"
   59.74  proof -
   59.75 -  interpret I: finite_product_sigma_finite M "{i}" by default simp
   59.76 +  interpret I: finite_product_sigma_finite M "{i}" by standard simp
   59.77    from f show ?thesis
   59.78      apply (subst distr_singleton[symmetric])
   59.79      apply (subst nn_integral_distr[OF measurable_component_singleton])
   59.80 @@ -970,8 +970,8 @@
   59.81      and f: "f \<in> borel_measurable (Pi\<^sub>M (insert i I) M)"
   59.82    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))"
   59.83  proof -
   59.84 -  interpret I: finite_product_sigma_finite M I by default auto
   59.85 -  interpret i: finite_product_sigma_finite M "{i}" by default auto
   59.86 +  interpret I: finite_product_sigma_finite M I by standard auto
   59.87 +  interpret i: finite_product_sigma_finite M "{i}" by standard auto
   59.88    have IJ: "I \<inter> {i} = {}" and insert: "I \<union> {i} = insert i I"
   59.89      using f by auto
   59.90    show ?thesis
   59.91 @@ -1008,7 +1008,7 @@
   59.92  using assms proof induct
   59.93    case (insert i I)
   59.94    note `finite I`[intro, simp]
   59.95 -  interpret I: finite_product_sigma_finite M I by default auto
   59.96 +  interpret I: finite_product_sigma_finite M I by standard auto
   59.97    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))"
   59.98      using insert by (auto intro!: setprod.cong)
   59.99    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)"
  59.100 @@ -1044,7 +1044,7 @@
  59.101  lemma (in product_sigma_finite) distr_component:
  59.102    "distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P")
  59.103  proof (intro measure_eqI[symmetric])
  59.104 -  interpret I: finite_product_sigma_finite M "{i}" by default simp
  59.105 +  interpret I: finite_product_sigma_finite M "{i}" by standard simp
  59.106  
  59.107    have eq: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x"
  59.108      by (auto simp: extensional_def restrict_def)
  59.109 @@ -1068,8 +1068,8 @@
  59.110      and emeasure_fold_measurable:
  59.111      "(\<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)
  59.112  proof -
  59.113 -  interpret I: finite_product_sigma_finite M I by default fact
  59.114 -  interpret J: finite_product_sigma_finite M J by default fact
  59.115 +  interpret I: finite_product_sigma_finite M I by standard fact
  59.116 +  interpret J: finite_product_sigma_finite M J by standard fact
  59.117    interpret IJ: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" ..
  59.118    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)"
  59.119      by (intro measurable_sets[OF _ A] measurable_merge assms)
    60.1 --- a/src/HOL/Probability/Giry_Monad.thy	Sun Sep 13 22:25:21 2015 +0200
    60.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Sun Sep 13 22:56:52 2015 +0200
    60.3 @@ -25,7 +25,7 @@
    60.4    proof
    60.5      show "emeasure M (space M) \<noteq> \<infinity>" using * by auto
    60.6    qed
    60.7 -  show "subprob_space M" by default fact+
    60.8 +  show "subprob_space M" by standard fact+
    60.9  qed
   60.10  
   60.11  lemma prob_space_imp_subprob_space:
    61.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Sun Sep 13 22:25:21 2015 +0200
    61.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Sun Sep 13 22:56:52 2015 +0200
    61.3 @@ -50,8 +50,8 @@
    61.4  
    61.5      have "finite (K - J)" using K by auto
    61.6  
    61.7 -    interpret J: finite_product_prob_space M J by default fact+
    61.8 -    interpret KmJ: finite_product_prob_space M "K - J" by default fact+
    61.9 +    interpret J: finite_product_prob_space M J by standard fact+
   61.10 +    interpret KmJ: finite_product_prob_space M "K - J" by standard fact+
   61.11  
   61.12      have "\<mu>G Z = emeasure (Pi\<^sub>M (J \<union> (K - J)) M) (emb (J \<union> (K - J)) K X)"
   61.13        using K J by simp
   61.14 @@ -84,7 +84,7 @@
   61.15    proof (rule G.caratheodory_empty_continuous[OF positive_mu_G additive_mu_G])
   61.16      fix A assume "A \<in> ?G"
   61.17      with generatorE guess J X . note JX = this
   61.18 -    interpret JK: finite_product_prob_space M J by default fact+ 
   61.19 +    interpret JK: finite_product_prob_space M J by standard fact+ 
   61.20      from JX show "\<mu>G A \<noteq> \<infinity>" by simp
   61.21    next
   61.22      fix A assume A: "range A \<subseteq> ?G" "decseq A" "(\<Inter>i. A i) = {}"
   61.23 @@ -113,7 +113,7 @@
   61.24        have J_mono: "\<And>n m. n \<le> m \<Longrightarrow> J n \<subseteq> J m"
   61.25          unfolding J_def by force
   61.26  
   61.27 -      interpret J: finite_product_prob_space M "J i" for i by default fact+
   61.28 +      interpret J: finite_product_prob_space M "J i" for i by standard fact+
   61.29  
   61.30        have a_le_1: "?a \<le> 1"
   61.31          using mu_G_spec[of "J 0" "A 0" "X 0"] J A_eq
   61.32 @@ -124,7 +124,7 @@
   61.33        { fix Z k assume Z: "range Z \<subseteq> ?G" "decseq Z" "\<forall>n. ?a / 2^k \<le> \<mu>G (Z n)"
   61.34          then have Z_sets: "\<And>n. Z n \<in> ?G" by auto
   61.35          fix J' assume J': "J' \<noteq> {}" "finite J'" "J' \<subseteq> I"
   61.36 -        interpret J': finite_product_prob_space M J' by default fact+
   61.37 +        interpret J': finite_product_prob_space M J' by standard fact+
   61.38  
   61.39          let ?q = "\<lambda>n y. \<mu>G (?M J' (Z n) y)"
   61.40          let ?Q = "\<lambda>n. ?q n -` {?a / 2^(k+1) ..} \<inter> space (Pi\<^sub>M J' M)"
    62.1 --- a/src/HOL/Probability/Information.thy	Sun Sep 13 22:25:21 2015 +0200
    62.2 +++ b/src/HOL/Probability/Information.thy	Sun Sep 13 22:56:52 2015 +0200
    62.3 @@ -311,7 +311,7 @@
    62.4    shows "0 \<le> KL_divergence b (density M f) (density M g)"
    62.5  proof -
    62.6    interpret Mf: prob_space "density M f" by fact
    62.7 -  interpret Mf: information_space "density M f" b by default fact
    62.8 +  interpret Mf: information_space "density M f" b by standard fact
    62.9    have eq: "density (density M f) (\<lambda>x. g x / f x) = density M g" (is "?DD = _")
   62.10      using f g ac by (subst density_density_divide) simp_all
   62.11  
   62.12 @@ -443,8 +443,8 @@
   62.13      by (rule prob_space_distr) fact
   62.14    interpret Y: prob_space "distr M T Y"
   62.15      by (rule prob_space_distr) fact
   62.16 -  interpret XY: pair_prob_space "distr M S X" "distr M T Y" by default
   62.17 -  interpret P: information_space P b unfolding P_def by default (rule b_gt_1)
   62.18 +  interpret XY: pair_prob_space "distr M S X" "distr M T Y" by standard
   62.19 +  interpret P: information_space P b unfolding P_def by standard (rule b_gt_1)
   62.20  
   62.21    interpret Q: prob_space Q unfolding Q_def
   62.22      by (rule prob_space_distr) simp
   62.23 @@ -770,7 +770,7 @@
   62.24    interpret X: prob_space "distr M S X"
   62.25      using D(1) by (rule prob_space_distr)
   62.26  
   62.27 -  have sf: "sigma_finite_measure (distr M S X)" by default
   62.28 +  have sf: "sigma_finite_measure (distr M S X)" by standard
   62.29    show ?thesis
   62.30      using D
   62.31      apply (subst eq_commute)
    63.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Sun Sep 13 22:25:21 2015 +0200
    63.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Sun Sep 13 22:56:52 2015 +0200
    63.3 @@ -2454,7 +2454,7 @@
    63.4  
    63.5  lemma (in finite_measure) finite_measure_restricted:
    63.6    "S \<in> sets M \<Longrightarrow> finite_measure (density M (indicator S))"
    63.7 -  by default (simp add: emeasure_restricted)
    63.8 +  by standard (simp add: emeasure_restricted)
    63.9  
   63.10  lemma emeasure_density_const:
   63.11    "A \<in> sets M \<Longrightarrow> 0 \<le> c \<Longrightarrow> emeasure (density M (\<lambda>_. c)) A = c * emeasure M A"
    64.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Sun Sep 13 22:25:21 2015 +0200
    64.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Sun Sep 13 22:56:52 2015 +0200
    64.3 @@ -653,7 +653,7 @@
    64.4      measure (density (count_space UNIV) (ereal \<circ> f)) {x} \<noteq> 0"
    64.5      by (simp add: AE_density nonneg measure_def emeasure_density max_def)
    64.6    show "prob_space (density (count_space UNIV) (ereal \<circ> f))"
    64.7 -    by default (simp add: emeasure_density prob)
    64.8 +    by standard (simp add: emeasure_density prob)
    64.9  qed simp
   64.10  
   64.11  lemma pmf_embed_pmf: "pmf embed_pmf x = f x"
    65.1 --- a/src/HOL/Probability/Probability_Measure.thy	Sun Sep 13 22:25:21 2015 +0200
    65.2 +++ b/src/HOL/Probability/Probability_Measure.thy	Sun Sep 13 22:56:52 2015 +0200
    65.3 @@ -20,7 +20,7 @@
    65.4    proof
    65.5      show "emeasure M (space M) \<noteq> \<infinity>" using * by simp 
    65.6    qed
    65.7 -  show "prob_space M" by default fact
    65.8 +  show "prob_space M" by standard fact
    65.9  qed
   65.10  
   65.11  lemma prob_space_imp_sigma_finite: "prob_space M \<Longrightarrow> sigma_finite_measure M"
   65.12 @@ -626,7 +626,7 @@
   65.13  proof safe
   65.14    interpret S: sigma_finite_measure S by fact
   65.15    interpret T: sigma_finite_measure T by fact
   65.16 -  interpret ST: pair_sigma_finite S T by default
   65.17 +  interpret ST: pair_sigma_finite S T ..
   65.18  
   65.19    from ST.sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('b \<times> 'c) set" .. note F = this
   65.20    let ?E = "{a \<times> b |a b. a \<in> sets S \<and> b \<in> sets T}"
   65.21 @@ -666,8 +666,8 @@
   65.22  proof -
   65.23    interpret S: sigma_finite_measure S by fact
   65.24    interpret T: sigma_finite_measure T by fact
   65.25 -  interpret ST: pair_sigma_finite S T by default
   65.26 -  interpret TS: pair_sigma_finite T S by default
   65.27 +  interpret ST: pair_sigma_finite S T ..
   65.28 +  interpret TS: pair_sigma_finite T S ..
   65.29  
   65.30    note Pxy[measurable]
   65.31    show ?thesis 
   65.32 @@ -715,7 +715,7 @@
   65.33  proof safe
   65.34    interpret S: sigma_finite_measure S by fact
   65.35    interpret T: sigma_finite_measure T by fact
   65.36 -  interpret ST: pair_sigma_finite S T by default
   65.37 +  interpret ST: pair_sigma_finite S T ..
   65.38  
   65.39    note Pxy[measurable]
   65.40    show X: "X \<in> measurable M S" by simp
   65.41 @@ -792,7 +792,7 @@
   65.42  proof safe
   65.43    interpret S: sigma_finite_measure S by fact
   65.44    interpret T: sigma_finite_measure T by fact
   65.45 -  interpret ST: pair_sigma_finite S T by default
   65.46 +  interpret ST: pair_sigma_finite S T ..
   65.47  
   65.48    interpret X: prob_space "density S Px"
   65.49      unfolding distributed_distr_eq_density[OF X, symmetric]
   65.50 @@ -1133,7 +1133,7 @@
   65.51  qed
   65.52  
   65.53  lemma prob_space_uniform_count_measure: "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> prob_space (uniform_count_measure A)"
   65.54 -  by default (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def)
   65.55 +  by standard (auto simp: emeasure_uniform_count_measure space_uniform_count_measure one_ereal_def)
   65.56  
   65.57  lemma (in prob_space) measure_uniform_measure_eq_cond_prob:
   65.58    assumes [measurable]: "Measurable.pred M P" "Measurable.pred M Q"
    66.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Sun Sep 13 22:25:21 2015 +0200
    66.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Sun Sep 13 22:56:52 2015 +0200
    66.3 @@ -993,7 +993,7 @@
    66.4    note A_in_sets = this
    66.5  
    66.6    show "sigma_finite_measure ?N"
    66.7 -  proof (default, intro exI conjI ballI)
    66.8 +  proof (standard, intro exI conjI ballI)
    66.9      show "countable (range (\<lambda>(i, j). A i \<inter> Q j))"
   66.10        by auto
   66.11      show "range (\<lambda>(i, j). A i \<inter> Q j) \<subseteq> sets (density M f)"
    67.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Sun Sep 13 22:25:21 2015 +0200
    67.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Sun Sep 13 22:56:52 2015 +0200
    67.3 @@ -1333,7 +1333,7 @@
    67.4    assumes "N \<subseteq> M"
    67.5    shows "dynkin \<Omega> N \<subseteq> M"
    67.6  proof -
    67.7 -  have "dynkin_system \<Omega> M" by default
    67.8 +  have "dynkin_system \<Omega> M" ..
    67.9    then have "dynkin_system \<Omega> M"
   67.10      using assms unfolding dynkin_system_def dynkin_system_axioms_def subset_class_def by simp
   67.11    with `N \<subseteq> M` show ?thesis by (auto simp add: dynkin_def)
   67.12 @@ -1432,7 +1432,7 @@
   67.13      using closed by (rule sigma_algebra_sigma_sets)
   67.14    from compl[OF _ empty] closed have space: "P \<Omega>" by simp
   67.15    interpret dynkin_system \<Omega> ?D
   67.16 -    by default (auto dest: sets_into_space intro!: space compl union)
   67.17 +    by standard (auto dest: sets_into_space intro!: space compl union)
   67.18    have "sigma_sets \<Omega> G = ?D"
   67.19      by (rule dynkin_lemma) (auto simp: basic `Int_stable G`)
   67.20    with A show ?thesis by auto
   67.21 @@ -1967,7 +1967,7 @@
   67.22    assume "\<not> (\<forall>i\<in>I. \<mu> i = 0)"
   67.23    moreover
   67.24    have "measure_space (space M) (sets M) \<mu>'"
   67.25 -    using ms unfolding measure_space_def by auto default
   67.26 +    using ms unfolding measure_space_def by auto standard
   67.27    with ms eq have "\<exists>\<mu>'. P \<mu>'"
   67.28      unfolding P_def
   67.29      by (intro exI[of _ \<mu>']) (auto simp add: M space_extend_measure sets_extend_measure)
    68.1 --- a/src/HOL/Probability/Stream_Space.thy	Sun Sep 13 22:25:21 2015 +0200
    68.2 +++ b/src/HOL/Probability/Stream_Space.thy	Sun Sep 13 22:56:52 2015 +0200
    68.3 @@ -160,7 +160,7 @@
    68.4  
    68.5  lemma (in prob_space) prob_space_stream_space: "prob_space (stream_space M)"
    68.6  proof -
    68.7 -  interpret product_prob_space "\<lambda>_. M" UNIV by default
    68.8 +  interpret product_prob_space "\<lambda>_. M" UNIV ..
    68.9    show ?thesis
   68.10      by (subst stream_space_eq_distr) (auto intro!: P.prob_space_distr)
   68.11  qed
   68.12 @@ -169,10 +169,8 @@
   68.13    assumes [measurable]: "f \<in> borel_measurable (stream_space M)"
   68.14    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)"
   68.15  proof -                  
   68.16 -  interpret S: sequence_space M
   68.17 -    by default
   68.18 -  interpret P: pair_sigma_finite M "\<Pi>\<^sub>M i::nat\<in>UNIV. M"
   68.19 -    by default
   68.20 +  interpret S: sequence_space M ..
   68.21 +  interpret P: pair_sigma_finite M "\<Pi>\<^sub>M i::nat\<in>UNIV. M" ..
   68.22  
   68.23    have "(\<integral>\<^sup>+X. f X \<partial>stream_space M) = (\<integral>\<^sup>+X. f (to_stream X) \<partial>S.S)"
   68.24      by (subst stream_space_eq_distr) (simp add: nn_integral_distr)
    69.1 --- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Sun Sep 13 22:25:21 2015 +0200
    69.2 +++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Sun Sep 13 22:56:52 2015 +0200
    69.3 @@ -399,7 +399,7 @@
    69.4       (insert n_gt_3, auto simp: dc_crypto intro: exI[of _ "replicate n True"])
    69.5  
    69.6  sublocale dining_cryptographers_space \<subseteq> information_space "uniform_count_measure dc_crypto" 2
    69.7 -  by default auto
    69.8 +  by standard auto
    69.9  
   69.10  notation (in dining_cryptographers_space)
   69.11    mutual_information_Pow ("\<I>'( _ ; _ ')")
    70.1 --- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Sun Sep 13 22:25:21 2015 +0200
    70.2 +++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Sun Sep 13 22:56:52 2015 +0200
    70.3 @@ -125,10 +125,10 @@
    70.4     by (auto intro!: setsum_nonneg)
    70.5  
    70.6  sublocale finite_information \<subseteq> prob_space "point_measure \<Omega> p"
    70.7 -  by default (simp add: one_ereal_def emeasure_point_measure_finite)
    70.8 +  by standard (simp add: one_ereal_def emeasure_point_measure_finite)
    70.9  
   70.10  sublocale finite_information \<subseteq> information_space "point_measure \<Omega> p" b
   70.11 -  by default simp
   70.12 +  by standard simp
   70.13  
   70.14  lemma (in finite_information) \<mu>'_eq: "A \<subseteq> \<Omega> \<Longrightarrow> prob A = setsum p A"
   70.15    by (auto simp: measure_point_measure)
   70.16 @@ -150,7 +150,7 @@
   70.17  end
   70.18  
   70.19  sublocale koepf_duermuth \<subseteq> finite_information msgs P b
   70.20 -proof default
   70.21 +proof
   70.22    show "finite msgs" unfolding msgs_def
   70.23      using finite_lists_length_eq[OF M.finite_space, of n]
   70.24      by auto
    71.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Sun Sep 13 22:25:21 2015 +0200
    71.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Sun Sep 13 22:56:52 2015 +0200
    71.3 @@ -478,8 +478,8 @@
    71.4    fixes R
    71.5    assumes "R x y --> R y x --> x = y"
    71.6  
    71.7 -interpretation equal : antisym "op =" by default simp
    71.8 -interpretation order_nat : antisym "op <= :: nat => _ => _" by default simp
    71.9 +interpretation equal : antisym "op =" by standard simp
   71.10 +interpretation order_nat : antisym "op <= :: nat => _ => _" by standard simp
   71.11  
   71.12  lemma (in antisym)
   71.13    "R x y --> R y z --> R x z"
    72.1 --- a/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy	Sun Sep 13 22:25:21 2015 +0200
    72.2 +++ b/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy	Sun Sep 13 22:56:52 2015 +0200
    72.3 @@ -91,7 +91,7 @@
    72.4  
    72.5  datatype ('a::finite, 'b::finite) F = F 'a | F2 'b
    72.6  
    72.7 -instance T :: (finite) finite by (default, transfer, auto)
    72.8 +instance T :: (finite) finite by standard (transfer, auto)
    72.9  
   72.10  lift_definition(code_dt) f17 :: "bool \<Rightarrow> (bool T, 'b::finite) F" is "\<lambda>b. F b" by auto
   72.11  
    73.1 --- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Sun Sep 13 22:25:21 2015 +0200
    73.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Sun Sep 13 22:56:52 2015 +0200
    73.3 @@ -188,8 +188,7 @@
    73.4    "(sup :: int \<Rightarrow> int \<Rightarrow> int) = max"
    73.5  
    73.6  instance
    73.7 -  by default
    73.8 -     (auto simp add: inf_int_def sup_int_def max_min_distrib2)
    73.9 +  by standard (auto simp add: inf_int_def sup_int_def max_min_distrib2)
   73.10  
   73.11  end
   73.12  
    74.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Sep 13 22:25:21 2015 +0200
    74.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Sun Sep 13 22:56:52 2015 +0200
    74.3 @@ -1294,7 +1294,7 @@
    74.4    assumes "\<And>x y. f (x + y) = f x + f y"
    74.5    assumes "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
    74.6    shows "linear f"
    74.7 -  by default (rule assms)+
    74.8 +  by standard (rule assms)+
    74.9  
   74.10  locale bounded_linear = linear f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" +
   74.11    assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
   74.12 @@ -1334,7 +1334,7 @@
   74.13    assumes "\<And>r x. f (scaleR r x) = scaleR r (f x)"
   74.14    assumes "\<And>x. norm (f x) \<le> norm x * K"
   74.15    shows "bounded_linear f"
   74.16 -  by default (fast intro: assms)+
   74.17 +  by standard (fast intro: assms)+
   74.18  
   74.19  locale bounded_bilinear =
   74.20    fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector]
   74.21 @@ -1415,10 +1415,10 @@
   74.22  end
   74.23  
   74.24  lemma bounded_linear_ident[simp]: "bounded_linear (\<lambda>x. x)"
   74.25 -  by default (auto intro!: exI[of _ 1])
   74.26 +  by standard (auto intro!: exI[of _ 1])
   74.27  
   74.28  lemma bounded_linear_zero[simp]: "bounded_linear (\<lambda>x. 0)"
   74.29 -  by default (auto intro!: exI[of _ 1])
   74.30 +  by standard (auto intro!: exI[of _ 1])
   74.31  
   74.32  lemma bounded_linear_add:
   74.33    assumes "bounded_linear f"
   74.34 @@ -1859,7 +1859,7 @@
   74.35  
   74.36  class banach = real_normed_vector + complete_space
   74.37  
   74.38 -instance real :: banach by default
   74.39 +instance real :: banach ..
   74.40  
   74.41  lemma tendsto_at_topI_sequentially:
   74.42    fixes f :: "real \<Rightarrow> 'b::first_countable_topology"
    75.1 --- a/src/HOL/Relation.thy	Sun Sep 13 22:25:21 2015 +0200
    75.2 +++ b/src/HOL/Relation.thy	Sun Sep 13 22:56:52 2015 +0200
    75.3 @@ -1116,7 +1116,7 @@
    75.4    assumes "finite A"
    75.5    shows "Id_on A = Finite_Set.fold (\<lambda>x. Set.insert (Pair x x)) {} A"
    75.6  proof -
    75.7 -  interpret comp_fun_commute "\<lambda>x. Set.insert (Pair x x)" by default auto
    75.8 +  interpret comp_fun_commute "\<lambda>x. Set.insert (Pair x x)" by standard auto
    75.9    show ?thesis using assms unfolding Id_on_def by (induct A) simp_all
   75.10  qed
   75.11  
   75.12 @@ -1126,7 +1126,7 @@
   75.13    interpret comp_fun_idem Set.insert
   75.14        by (fact comp_fun_idem_insert)
   75.15    show ?thesis 
   75.16 -  by default (auto simp add: fun_eq_iff comp_fun_commute split:prod.split)
   75.17 +  by standard (auto simp add: fun_eq_iff comp_fun_commute split:prod.split)
   75.18  qed
   75.19  
   75.20  lemma Image_fold:
   75.21 @@ -1148,7 +1148,7 @@
   75.22    proof - 
   75.23      interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
   75.24      show "comp_fun_commute (\<lambda>(w,z) A'. if snd x = w then Set.insert (fst x,z) A' else A')"
   75.25 -    by default (auto simp add: fun_eq_iff split:prod.split)
   75.26 +    by standard (auto simp add: fun_eq_iff split:prod.split)
   75.27    qed
   75.28    have *: "{x} O S = {(x', z). x' = fst x \<and> (snd x,z) \<in> S}" by (auto simp: relcomp_unfold intro!: exI)
   75.29    show ?thesis unfolding *
   75.30 @@ -1172,7 +1172,7 @@
   75.31    have *: "\<And>a b A. 
   75.32      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"
   75.33      by (auto simp: insert_relcomp_union_fold[OF assms] cong: if_cong)
   75.34 -  show ?thesis by default (auto simp: *)
   75.35 +  show ?thesis by standard (auto simp: *)
   75.36  qed
   75.37  
   75.38  lemma relcomp_fold:
    76.1 --- a/src/HOL/Topological_Spaces.thy	Sun Sep 13 22:25:21 2015 +0200
    76.2 +++ b/src/HOL/Topological_Spaces.thy	Sun Sep 13 22:56:52 2015 +0200
    76.3 @@ -212,7 +212,7 @@
    76.4  
    76.5  lemma topological_space_generate_topology:
    76.6    "class.topological_space (generate_topology S)"
    76.7 -  by default (auto intro: generate_topology.intros)
    76.8 +  by standard (auto intro: generate_topology.intros)
    76.9  
   76.10  subsection \<open>Order topologies\<close>
   76.11  
    77.1 --- a/src/HOL/UNITY/Follows.thy	Sun Sep 13 22:25:21 2015 +0200
    77.2 +++ b/src/HOL/UNITY/Follows.thy	Sun Sep 13 22:56:52 2015 +0200
    77.3 @@ -179,7 +179,7 @@
    77.4     "(M'::'a multiset) \<le> M \<longleftrightarrow> M' #<=# M"
    77.5  
    77.6  instance
    77.7 -  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)
    77.8 +  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)
    77.9  end
   77.10  
   77.11  lemma increasing_union: 
    78.1 --- a/src/HOL/UNITY/Guar.thy	Sun Sep 13 22:25:21 2015 +0200
    78.2 +++ b/src/HOL/UNITY/Guar.thy	Sun Sep 13 22:56:52 2015 +0200
    78.3 @@ -17,7 +17,7 @@
    78.4  begin
    78.5  
    78.6  instance program :: (type) order
    78.7 -  by default (auto simp add: program_less_le dest: component_antisym intro: component_trans)
    78.8 +  by standard (auto simp add: program_less_le dest: component_antisym intro: component_trans)
    78.9  
   78.10  text{*Existential and Universal properties.  I formalize the two-program
   78.11        case, proving equivalence with Chandy and Sanders's n-ary definitions*}
    79.1 --- a/src/HOL/Word/Word.thy	Sun Sep 13 22:25:21 2015 +0200
    79.2 +++ b/src/HOL/Word/Word.thy	Sun Sep 13 22:56:52 2015 +0200
    79.3 @@ -313,7 +313,7 @@
    79.4    word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
    79.5  
    79.6  instance
    79.7 -  by default (transfer, simp add: algebra_simps)+
    79.8 +  by standard (transfer, simp add: algebra_simps)+
    79.9  
   79.10  end
   79.11  
   79.12 @@ -384,7 +384,7 @@
   79.13    word_less_def: "a < b \<longleftrightarrow> uint a < uint b"
   79.14  
   79.15  instance
   79.16 -  by default (auto simp: word_less_def word_le_def)
   79.17 +  by standard (auto simp: word_less_def word_le_def)
   79.18  
   79.19  end
   79.20  
   79.21 @@ -1194,7 +1194,7 @@
   79.22    by (fact word_less_def)
   79.23  
   79.24  lemma signed_linorder: "class.linorder word_sle word_sless"
   79.25 -  by default (unfold word_sle_def word_sless_def, auto)
   79.26 +  by standard (unfold word_sle_def word_sless_def, auto)
   79.27  
   79.28  interpretation signed: linorder "word_sle" "word_sless"
   79.29    by (rule signed_linorder)
   79.30 @@ -2215,7 +2215,7 @@
   79.31  subsection {* Cardinality, finiteness of set of words *}
   79.32  
   79.33  instance word :: (len0) finite
   79.34 -  by (default, simp add: type_definition.univ [OF type_definition_word])
   79.35 +  by standard (simp add: type_definition.univ [OF type_definition_word])
   79.36  
   79.37  lemma card_word: "CARD('a::len0 word) = 2 ^ len_of TYPE('a)"
   79.38    by (simp add: type_definition.card [OF type_definition_word] nat_power_eq)
    80.1 --- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Sun Sep 13 22:25:21 2015 +0200
    80.2 +++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Sun Sep 13 22:56:52 2015 +0200
    80.3 @@ -88,7 +88,7 @@
    80.4    "perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"
    80.5  
    80.6  typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
    80.7 -  by (default) (auto simp: perms_def)
    80.8 +  by standard (auto simp: perms_def)
    80.9  
   80.10  text {*First we need some auxiliary lemmas.*}
   80.11  lemma permsI [Pure.intro]:
   80.12 @@ -153,13 +153,14 @@
   80.13    unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm)
   80.14  
   80.15  instance
   80.16 -  apply default
   80.17 +  apply standard
   80.18    unfolding Rep_perm_inject [symmetric]
   80.19    unfolding minus_perm_def
   80.20    unfolding Rep_perm_add
   80.21    unfolding Rep_perm_uminus
   80.22    unfolding Rep_perm_0
   80.23 -  by (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])
   80.24 +  apply (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])
   80.25 +  done
   80.26  
   80.27  end
   80.28  
   80.29 @@ -198,7 +199,7 @@
   80.30    PERMUTE permute_atom
   80.31  
   80.32  interpretation atom_permute: permute permute_atom
   80.33 -  by (default) (simp add: permute_atom_def Rep_perm_simps)+
   80.34 +  by standard (simp_all add: permute_atom_def Rep_perm_simps)
   80.35  
   80.36  text {*Permuting permutations.*}
   80.37  definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where
   80.38 @@ -208,7 +209,7 @@
   80.39    PERMUTE permute_perm
   80.40  
   80.41  interpretation perm_permute: permute permute_perm
   80.42 -  apply default
   80.43 +  apply standard
   80.44    unfolding permute_perm_def
   80.45    apply simp
   80.46    apply (simp only: diff_conv_add_uminus minus_add add.assoc)
    81.1 --- a/src/HOL/ex/Dedekind_Real.thy	Sun Sep 13 22:25:21 2015 +0200
    81.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Sun Sep 13 22:56:52 2015 +0200
    81.3 @@ -1567,7 +1567,7 @@
    81.4    "(sup :: real \<Rightarrow> real \<Rightarrow> real) = max"
    81.5  
    81.6  instance
    81.7 -  by default (auto simp add: inf_real_def sup_real_def max_min_distrib2)
    81.8 +  by standard (auto simp add: inf_real_def sup_real_def max_min_distrib2)
    81.9  
   81.10  end
   81.11