# HG changeset patch
# User wenzelm
# Date 1436216254 -7200
# Node ID ade12ef2773c53605eec77a21b58bb34afd6c961
# Parent  17ba2df56dee0eb041a05ca34cdf10fef97cc7fa
tuned proofs;

diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Bit.thy
--- a/src/HOL/Library/Bit.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Bit.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -123,8 +123,8 @@
   plus_bit_def times_bit_def minus_bit_def uminus_bit_def
   divide_bit_def inverse_bit_def
 
-instance proof
-qed (unfold field_bit_defs, auto split: bit.split)
+instance
+  by standard (auto simp: field_bit_defs split: bit.split)
 
 end
 
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Cardinality.thy
--- a/src/HOL/Library/Cardinality.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Cardinality.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -228,19 +228,21 @@
 instantiation natural :: card_UNIV begin
 definition "finite_UNIV = Phantom(natural) False"
 definition "card_UNIV = Phantom(natural) 0"
-instance proof
-qed (auto simp add: finite_UNIV_natural_def card_UNIV_natural_def card_eq_0_iff
-  type_definition.univ [OF type_definition_natural] natural_eq_iff
-  dest!: finite_imageD intro: inj_onI)
+instance
+  by standard
+    (auto simp add: finite_UNIV_natural_def card_UNIV_natural_def card_eq_0_iff
+      type_definition.univ [OF type_definition_natural] natural_eq_iff
+      dest!: finite_imageD intro: inj_onI)
 end
 
 instantiation integer :: card_UNIV begin
 definition "finite_UNIV = Phantom(integer) False"
 definition "card_UNIV = Phantom(integer) 0"
-instance proof
-qed (auto simp add: finite_UNIV_integer_def card_UNIV_integer_def card_eq_0_iff
-  type_definition.univ [OF type_definition_integer] infinite_UNIV_int
-  dest!: finite_imageD intro: inj_onI)
+instance
+  by standard
+    (auto simp add: finite_UNIV_integer_def card_UNIV_integer_def card_eq_0_iff
+      type_definition.univ [OF type_definition_integer] infinite_UNIV_int
+      dest!: finite_imageD intro: inj_onI)
 end
 
 instantiation list :: (type) card_UNIV begin
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Char_ord.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -11,42 +11,33 @@
 instantiation nibble :: linorder
 begin
 
-definition
-  "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
+definition "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
+definition "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
 
-definition
-  "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
-
-instance proof
-qed (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
+instance
+  by standard (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
 
 end
 
 instantiation nibble :: distrib_lattice
 begin
 
-definition
-  "(inf \<Colon> nibble \<Rightarrow> _) = min"
+definition "(inf \<Colon> nibble \<Rightarrow> _) = min"
+definition "(sup \<Colon> nibble \<Rightarrow> _) = max"
 
-definition
-  "(sup \<Colon> nibble \<Rightarrow> _) = max"
-
-instance proof
-qed (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
+instance
+  by standard (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
 
 end
 
 instantiation char :: linorder
 begin
 
-definition
-  "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
+definition "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
+definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
 
-definition
-  "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
-
-instance proof
-qed (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
+instance
+  by standard (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
 
 end
 
@@ -83,14 +74,11 @@
 instantiation char :: distrib_lattice
 begin
 
-definition
-  "(inf \<Colon> char \<Rightarrow> _) = min"
+definition "(inf \<Colon> char \<Rightarrow> _) = min"
+definition "(sup \<Colon> char \<Rightarrow> _) = max"
 
-definition
-  "(sup \<Colon> char \<Rightarrow> _) = max"
-
-instance proof
-qed (auto simp add: inf_char_def sup_char_def max_min_distrib2)
+instance
+  by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
 
 end
 
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Countable_Set_Type.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -94,7 +94,8 @@
 lift_definition minus_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset"
 is minus parametric Diff_transfer by simp
 
-instance by default(transfer, fastforce)+
+instance by standard (transfer; auto)+
+
 end
 
 abbreviation cempty :: "'a cset" where "cempty \<equiv> bot"
@@ -536,14 +537,15 @@
 
 lemma finite_countable_subset:
 "finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
-apply default
+apply (rule iffI)
  apply (erule contrapos_pp)
  apply (rule card_of_ordLeq_infinite)
  apply (rule ordLeq_countable_subsets)
  apply assumption
 apply (rule finite_Collect_conjI)
 apply (rule disjI1)
-by (erule finite_Collect_subsets)
+apply (erule finite_Collect_subsets)
+done
 
 lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A"
   including cset.lifting
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/DAList.thy
--- a/src/HOL/Library/DAList.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/DAList.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -93,7 +93,7 @@
 definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
 
 instance
-  by default (simp add: equal_alist_def impl_of_inject)
+  by standard (simp add: equal_alist_def impl_of_inject)
 
 end
 
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/DAList_Multiset.thy
--- a/src/HOL/Library/DAList_Multiset.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -390,7 +390,7 @@
 
 lemma size_fold: "size A = fold_mset (\<lambda>_. Suc) 0 A" (is "_ = fold_mset ?f _ _")
 proof -
-  interpret comp_fun_commute ?f by default auto
+  interpret comp_fun_commute ?f by standard auto
   show ?thesis by (induct A) auto
 qed
 
@@ -405,7 +405,7 @@
 
 lemma set_mset_fold: "set_mset A = fold_mset insert {} A" (is "_ = fold_mset ?f _ _")
 proof -
-  interpret comp_fun_commute ?f by default auto
+  interpret comp_fun_commute ?f by standard auto
   show ?thesis by (induct A) auto
 qed
 
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Dlist.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -120,15 +120,14 @@
 
 definition "HOL.equal dxs dys \<longleftrightarrow> HOL.equal (list_of_dlist dxs) (list_of_dlist dys)"
 
-instance proof
-qed (simp add: equal_dlist_def equal list_of_dlist_inject)
+instance
+  by standard (simp add: equal_dlist_def equal list_of_dlist_inject)
 
 end
 
 declare equal_dlist_def [code]
 
-lemma [code nbe]:
-  "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
+lemma [code nbe]: "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
   by (fact equal_refl)
 
 
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -34,8 +34,10 @@
  
 instantiation enat :: infinity
 begin
-  definition "\<infinity> = Abs_enat None"
-  instance proof qed
+
+definition "\<infinity> = Abs_enat None"
+instance ..
+
 end
 
 instance enat :: countable
@@ -156,7 +158,8 @@
     and "q + \<infinity> = \<infinity>"
   by (simp_all add: plus_enat_def split: enat.splits)
 
-instance proof
+instance
+proof
   fix n m q :: enat
   show "n + m + q = n + (m + q)"
     by (cases n m q rule: enat3_cases) auto
@@ -203,7 +206,8 @@
   unfolding times_enat_def zero_enat_def
   by (simp_all split: enat.split)
 
-instance proof
+instance
+proof
   fix a b c :: enat
   show "(a * b) * c = a * (b * c)"
     unfolding times_enat_def zero_enat_def
@@ -242,7 +246,8 @@
   apply (simp add: plus_1_eSuc eSuc_enat)
   done
 
-instance enat :: semiring_char_0 proof
+instance enat :: semiring_char_0
+proof
   have "inj enat" by (rule injI) simp
   then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat)
 qed
@@ -355,8 +360,8 @@
   "(\<infinity>::enat) < q \<longleftrightarrow> False"
   by simp_all
 
-instance by default
-  (auto simp add: less_eq_enat_def less_enat_def plus_enat_def split: enat.splits)
+instance
+  by standard (auto simp add: less_eq_enat_def less_enat_def plus_enat_def split: enat.splits)
 
 end
 
@@ -486,14 +491,11 @@
 instantiation enat :: "{order_bot, order_top}"
 begin
 
-definition bot_enat :: enat where
-  "bot_enat = 0"
+definition bot_enat :: enat where "bot_enat = 0"
+definition top_enat :: enat where "top_enat = \<infinity>"
 
-definition top_enat :: enat where
-  "top_enat = \<infinity>"
-
-instance proof
-qed (simp_all add: bot_enat_def top_enat_def)
+instance
+  by standard (simp_all add: bot_enat_def top_enat_def)
 
 end
 
@@ -502,10 +504,11 @@
   shows "finite A"
 proof (rule finite_subset)
   show "finite (enat ` {..n})" by blast
-
   have "A \<subseteq> {..enat n}" using le_fin by fastforce
   also have "\<dots> \<subseteq> enat ` {..n}"
-    by (rule subsetI) (case_tac x, auto)
+    apply (rule subsetI)
+    subgoal for x by (cases x) auto
+    done
   finally show "A \<subseteq> enat ` {..n}" .
 qed
 
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -257,7 +257,7 @@
 | "real_ereal \<infinity> = 0"
 | "real_ereal (-\<infinity>) = 0"
   by (auto intro: ereal_cases)
-termination by default (rule wf_empty)
+termination by standard (rule wf_empty)
 
 instance ..
 end
@@ -340,7 +340,7 @@
   with prems show P
    by (cases rule: ereal2_cases[of a b]) auto
 qed auto
-termination by default (rule wf_empty)
+termination by standard (rule wf_empty)
 
 lemma Infty_neq_0[simp]:
   "(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"
@@ -509,7 +509,7 @@
   using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
 
 instance ereal :: dense_linorder
-  by default (blast dest: ereal_dense2)
+  by standard (blast dest: ereal_dense2)
 
 instance ereal :: ordered_ab_semigroup_add
 proof
@@ -848,7 +848,7 @@
 | "sgn (\<infinity>::ereal) = 1"
 | "sgn (-\<infinity>::ereal) = -1"
 by (auto intro: ereal_cases)
-termination by default (rule wf_empty)
+termination by standard (rule wf_empty)
 
 function times_ereal where
   "ereal r * ereal p = ereal (r * p)"
@@ -1602,7 +1602,7 @@
 
 definition [simp]: "sup x y = (max x y :: ereal)"
 definition [simp]: "inf x y = (min x y :: ereal)"
-instance by default simp_all
+instance by standard simp_all
 
 end
 
@@ -1706,7 +1706,7 @@
   open_ereal_generated: "open_ereal = generate_topology (range lessThan \<union> range greaterThan)"
 
 instance
-  by default (simp add: open_ereal_generated)
+  by standard (simp add: open_ereal_generated)
 
 end
 
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/FSet.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -23,7 +23,7 @@
 (* FIXME transfer and right_total vs. bi_total *)
 instantiation fset :: (finite) finite
 begin
-instance by default (transfer, simp)
+instance by (standard; transfer; simp)
 end
 
 instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
@@ -54,7 +54,7 @@
   by simp
 
 instance
-by default (transfer, auto)+
+  by (standard; transfer; auto)+
 
 end
 
@@ -132,9 +132,12 @@
 instantiation fset :: (finite) complete_lattice 
 begin
 
-lift_definition top_fset :: "'a fset" is UNIV parametric right_total_UNIV_transfer UNIV_transfer by simp
+lift_definition top_fset :: "'a fset" is UNIV parametric right_total_UNIV_transfer UNIV_transfer
+  by simp
 
-instance by default (transfer, auto)+
+instance
+  by (standard; transfer; auto)
+
 end
 
 instantiation fset :: (finite) complete_boolean_algebra
@@ -143,7 +146,8 @@
 lift_definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" is uminus 
   parametric right_total_Compl_transfer Compl_transfer by simp
 
-instance by (default, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+
+instance
+  by (standard, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+
 
 end
 
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Finite_Lattice.thy
--- a/src/HOL/Library/Finite_Lattice.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Finite_Lattice.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -32,13 +32,13 @@
   by (auto simp: bot_def intro: Inf_fin.coboundedI)
 
 instance finite_lattice_complete \<subseteq> order_bot
-  by default (auto simp: finite_lattice_complete_bot_least)
+  by standard (auto simp: finite_lattice_complete_bot_least)
 
 lemma finite_lattice_complete_top_greatest: "(top::'a::finite_lattice_complete) \<ge> x"
   by (auto simp: top_def Sup_fin.coboundedI)
 
 instance finite_lattice_complete \<subseteq> order_top
-  by default (auto simp: finite_lattice_complete_top_greatest)
+  by standard (auto simp: finite_lattice_complete_top_greatest)
 
 instance finite_lattice_complete \<subseteq> bounded_lattice ..
 
@@ -124,7 +124,7 @@
   by (metis Sup_fold_sup finite_code)
 
 instance prod :: (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
-  by default (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
+  by standard (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
 
 text \<open>Functions with a finite domain and with a finite lattice as codomain
 already form a finite lattice.\<close>
@@ -146,7 +146,7 @@
   by (metis Sup_fold_sup finite_code)
 
 instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
-  by default (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
+  by standard (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
 
 
 subsection \<open>Finite Distributive Lattices\<close>
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Float.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -237,8 +237,8 @@
 where "sup_float a b = max a b"
 
 instance
-  by default
-     (transfer, simp_all add: inf_float_def sup_float_def real_of_float_min real_of_float_max)+
+  by (standard; transfer; simp add: inf_float_def sup_float_def real_of_float_min real_of_float_max)
+
 end
 
 lemma float_numeral[simp]: "real (numeral x :: float) = numeral x"
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -218,7 +218,7 @@
 qed
 
 instance fps :: (zero_neq_one) zero_neq_one
-  by default (simp add: expand_fps_eq)
+  by standard (simp add: expand_fps_eq)
 
 instance fps :: (semiring_0) semiring
 proof
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Function_Algebras.thy
--- a/src/HOL/Library/Function_Algebras.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Function_Algebras.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -62,46 +62,45 @@
 text \<open>Additive structures\<close>
 
 instance "fun" :: (type, semigroup_add) semigroup_add
-  by default (simp add: fun_eq_iff add.assoc)
+  by standard (simp add: fun_eq_iff add.assoc)
 
 instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
-  by default (simp_all add: fun_eq_iff)
+  by standard (simp_all add: fun_eq_iff)
 
 instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
-  by default (simp add: fun_eq_iff add.commute)
+  by standard (simp add: fun_eq_iff add.commute)
 
 instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
-  by default (simp_all add: fun_eq_iff diff_diff_eq)
+  by standard (simp_all add: fun_eq_iff diff_diff_eq)
 
 instance "fun" :: (type, monoid_add) monoid_add
-  by default (simp_all add: fun_eq_iff)
+  by standard (simp_all add: fun_eq_iff)
 
 instance "fun" :: (type, comm_monoid_add) comm_monoid_add
-  by default simp
+  by standard simp
 
 instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
 
 instance "fun" :: (type, group_add) group_add
-  by default
-    (simp_all add: fun_eq_iff)
+  by standard (simp_all add: fun_eq_iff)
 
 instance "fun" :: (type, ab_group_add) ab_group_add
-  by default simp_all
+  by standard simp_all
 
 
 text \<open>Multiplicative structures\<close>
 
 instance "fun" :: (type, semigroup_mult) semigroup_mult
-  by default (simp add: fun_eq_iff mult.assoc)
+  by standard (simp add: fun_eq_iff mult.assoc)
 
 instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
-  by default (simp add: fun_eq_iff mult.commute)
+  by standard (simp add: fun_eq_iff mult.commute)
 
 instance "fun" :: (type, monoid_mult) monoid_mult
-  by default (simp_all add: fun_eq_iff)
+  by standard (simp_all add: fun_eq_iff)
 
 instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
-  by default simp
+  by standard simp
 
 
 text \<open>Misc\<close>
@@ -109,19 +108,19 @@
 instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
 
 instance "fun" :: (type, mult_zero) mult_zero
-  by default (simp_all add: fun_eq_iff)
+  by standard (simp_all add: fun_eq_iff)
 
 instance "fun" :: (type, zero_neq_one) zero_neq_one
-  by default (simp add: fun_eq_iff)
+  by standard (simp add: fun_eq_iff)
 
 
 text \<open>Ring structures\<close>
 
 instance "fun" :: (type, semiring) semiring
-  by default (simp_all add: fun_eq_iff algebra_simps)
+  by standard (simp_all add: fun_eq_iff algebra_simps)
 
 instance "fun" :: (type, comm_semiring) comm_semiring
-  by default (simp add: fun_eq_iff  algebra_simps)
+  by standard (simp add: fun_eq_iff  algebra_simps)
 
 instance "fun" :: (type, semiring_0) semiring_0 ..
 
@@ -155,7 +154,7 @@
 instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
 
 instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel 
-  by default (auto simp add: times_fun_def algebra_simps)
+  by standard (auto simp add: times_fun_def algebra_simps)
 
 instance "fun" :: (type, semiring_char_0) semiring_char_0
 proof
@@ -180,23 +179,22 @@
 text \<open>Ordered structures\<close>
 
 instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
-  by default (auto simp add: le_fun_def intro: add_left_mono)
+  by standard (auto simp add: le_fun_def intro: add_left_mono)
 
 instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
 
 instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
-  by default (simp add: le_fun_def)
+  by standard (simp add: le_fun_def)
 
 instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
 
 instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
 
 instance "fun" :: (type, ordered_semiring) ordered_semiring
-  by default
-    (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
+  by standard (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
 
 instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
-  by default (fact mult_left_mono)
+  by standard (fact mult_left_mono)
 
 instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
 
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Inner_Product.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -199,6 +199,7 @@
   "f differentiable (at x within s) \<Longrightarrow> g differentiable at x within s \<Longrightarrow> (\<lambda>x. inner (f x) (g x)) differentiable at x within s"
   unfolding differentiable_def by (blast intro: has_derivative_inner)
 
+
 subsection \<open>Class instances\<close>
 
 instantiation real :: real_inner
@@ -206,7 +207,8 @@
 
 definition inner_real_def [simp]: "inner = op *"
 
-instance proof
+instance
+proof
   fix x y z r :: real
   show "inner x y = inner y x"
     unfolding inner_real_def by (rule mult.commute)
@@ -230,7 +232,8 @@
 definition inner_complex_def:
   "inner x y = Re x * Re y + Im x * Im y"
 
-instance proof
+instance
+proof
   fix x y z :: complex and r :: real
   show "inner x y = inner y x"
     unfolding inner_complex_def by (simp add: mult.commute)
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Lattice_Constructions.thy
--- a/src/HOL/Library/Lattice_Constructions.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Lattice_Constructions.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -51,16 +51,16 @@
   by (simp add: less_bot_def)
 
 instance
-  by default
+  by standard
     (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
 
 end
 
 instance bot :: (order) order
-  by default (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
+  by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
 
 instance bot :: (linorder) linorder
-  by default (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
+  by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
 
 instantiation bot :: (order) bot
 begin
@@ -88,7 +88,7 @@
         | Value v' \<Rightarrow> Value (inf v v')))"
 
 instance
-  by default (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
+  by standard (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
 
 end
 
@@ -106,7 +106,7 @@
         | Value v' \<Rightarrow> Value (sup v v')))"
 
 instance
-  by default (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
+  by standard (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
 
 end
 
@@ -158,16 +158,16 @@
   by (simp add: less_top_def)
 
 instance
-  by default
+  by standard
     (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
 
 end
 
 instance top :: (order) order
-  by default (auto simp add: less_eq_top_def less_top_def split: top.splits)
+  by standard (auto simp add: less_eq_top_def less_top_def split: top.splits)
 
 instance top :: (linorder) linorder
-  by default (auto simp add: less_eq_top_def less_top_def split: top.splits)
+  by standard (auto simp add: less_eq_top_def less_top_def split: top.splits)
 
 instantiation top :: (order) top
 begin
@@ -195,7 +195,7 @@
         | Value v' \<Rightarrow> Value (inf v v')))"
 
 instance
-  by default (auto simp add: inf_top_def less_eq_top_def split: top.splits)
+  by standard (auto simp add: inf_top_def less_eq_top_def split: top.splits)
 
 end
 
@@ -213,12 +213,12 @@
         | Value v' \<Rightarrow> Value (sup v v')))"
 
 instance
-  by default (auto simp add: sup_top_def less_eq_top_def split: top.splits)
+  by standard (auto simp add: sup_top_def less_eq_top_def split: top.splits)
 
 end
 
 instance top :: (lattice) bounded_lattice_top
-  by default (simp add: top_top_def)
+  by standard (simp add: top_top_def)
 
 
 subsection \<open>Values extended by a top and a bottom element\<close>
@@ -267,7 +267,7 @@
   by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
 
 instance
-  by default
+  by standard
     (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def
       split: flat_complete_lattice.splits)
 
@@ -313,7 +313,7 @@
     | Top \<Rightarrow> Top)"
 
 instance
-  by default
+  by standard
     (auto simp add: inf_flat_complete_lattice_def sup_flat_complete_lattice_def
       less_eq_flat_complete_lattice_def split: flat_complete_lattice.splits)
 
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/List_lexord.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -74,7 +74,7 @@
 definition "(sup \<Colon> 'a list \<Rightarrow> _) = max"
 
 instance
-  by default (auto simp add: inf_list_def sup_list_def max_min_distrib2)
+  by standard (auto simp add: inf_list_def sup_list_def max_min_distrib2)
 
 end
 
@@ -102,7 +102,7 @@
 definition "bot = []"
 
 instance
-  by default (simp add: bot_list_def)
+  by standard (simp add: bot_list_def)
 
 end
 
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Mapping.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -183,8 +183,8 @@
 definition
   "HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)"
 
-instance proof
-qed (unfold equal_mapping_def, transfer, auto)
+instance
+  by standard (unfold equal_mapping_def, transfer, auto)
 
 end
 
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -62,7 +62,7 @@
   have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N"
     unfolding mult_def by (blast intro: trancl_trans)
   show "class.order ?le ?less"
-    by default (auto simp add: le_multiset_def irrefl dest: trans)
+    by standard (auto simp add: le_multiset_def irrefl dest: trans)
 qed
 
 text \<open>The Dershowitz--Manna ordering:\<close>
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -192,8 +192,8 @@
 lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
   by (induct x, induct y) simp
 
-instance proof
-qed (simp_all add: num1_eq_iff)
+instance
+  by standard (simp_all add: num1_eq_iff)
 
 end
 
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Option_ord.thy
--- a/src/HOL/Library/Option_ord.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Option_ord.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -62,59 +62,61 @@
 lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"
   by (simp add: less_option_def)
 
-instance proof
-qed (auto simp add: less_eq_option_def less_option_def less_le_not_le elim: order_trans split: option.splits)
-
-end 
+instance
+  by standard
+    (auto simp add: less_eq_option_def less_option_def less_le_not_le
+      elim: order_trans split: option.splits)
 
-instance option :: (order) order proof
-qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
+end
 
-instance option :: (linorder) linorder proof
-qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
+instance option :: (order) order
+  by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)
+
+instance option :: (linorder) linorder
+  by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)
 
 instantiation option :: (order) order_bot
 begin
 
-definition bot_option where
-  "\<bottom> = None"
+definition bot_option where "\<bottom> = None"
 
-instance proof
-qed (simp add: bot_option_def)
+instance
+  by standard (simp add: bot_option_def)
 
 end
 
 instantiation option :: (order_top) order_top
 begin
 
-definition top_option where
-  "\<top> = Some \<top>"
+definition top_option where "\<top> = Some \<top>"
 
-instance proof
-qed (simp add: top_option_def less_eq_option_def split: option.split)
+instance
+  by standard (simp add: top_option_def less_eq_option_def split: option.split)
 
 end
 
-instance option :: (wellorder) wellorder proof
-  fix P :: "'a option \<Rightarrow> bool" and z :: "'a option"
+instance option :: (wellorder) wellorder
+proof
+  fix P :: "'a option \<Rightarrow> bool"
+  fix z :: "'a option"
   assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
   have "P None" by (rule H) simp
-  then have P_Some [case_names Some]:
-    "\<And>z. (\<And>x. z = Some x \<Longrightarrow> (P o Some) x) \<Longrightarrow> P z"
-  proof -
-    fix z
-    assume "\<And>x. z = Some x \<Longrightarrow> (P o Some) x"
-    with \<open>P None\<close> show "P z" by (cases z) simp_all
-  qed
-  show "P z" proof (cases z rule: P_Some)
+  then have P_Some [case_names Some]: "P z" if "\<And>x. z = Some x \<Longrightarrow> (P o Some) x" for z
+    using \<open>P None\<close> that by (cases z) simp_all
+  show "P z"
+  proof (cases z rule: P_Some)
     case (Some w)
-    show "(P o Some) w" proof (induct rule: less_induct)
+    show "(P o Some) w"
+    proof (induct rule: less_induct)
       case (less x)
-      have "P (Some x)" proof (rule H)
+      have "P (Some x)"
+      proof (rule H)
         fix y :: "'a option"
         assume "y < Some x"
-        show "P y" proof (cases y rule: P_Some)
-          case (Some v) with \<open>y < Some x\<close> have "v < x" by simp
+        show "P y"
+        proof (cases y rule: P_Some)
+          case (Some v)
+          with \<open>y < Some x\<close> have "v < x" by simp
           with less show "(P o Some) v" .
         qed
       qed
@@ -129,16 +131,13 @@
 definition inf_option where
   "x \<sqinter> y = (case x of None \<Rightarrow> None | Some x \<Rightarrow> (case y of None \<Rightarrow> None | Some y \<Rightarrow> Some (x \<sqinter> y)))"
 
-lemma inf_None_1 [simp, code]:
-  "None \<sqinter> y = None"
+lemma inf_None_1 [simp, code]: "None \<sqinter> y = None"
   by (simp add: inf_option_def)
 
-lemma inf_None_2 [simp, code]:
-  "x \<sqinter> None = None"
+lemma inf_None_2 [simp, code]: "x \<sqinter> None = None"
   by (cases x) (simp_all add: inf_option_def)
 
-lemma inf_Some [simp, code]:
-  "Some x \<sqinter> Some y = Some (x \<sqinter> y)"
+lemma inf_Some [simp, code]: "Some x \<sqinter> Some y = Some (x \<sqinter> y)"
   by (simp add: inf_option_def)
 
 instance ..
@@ -151,53 +150,42 @@
 definition sup_option where
   "x \<squnion> y = (case x of None \<Rightarrow> y | Some x' \<Rightarrow> (case y of None \<Rightarrow> x | Some y \<Rightarrow> Some (x' \<squnion> y)))"
 
-lemma sup_None_1 [simp, code]:
-  "None \<squnion> y = y"
+lemma sup_None_1 [simp, code]: "None \<squnion> y = y"
   by (simp add: sup_option_def)
 
-lemma sup_None_2 [simp, code]:
-  "x \<squnion> None = x"
+lemma sup_None_2 [simp, code]: "x \<squnion> None = x"
   by (cases x) (simp_all add: sup_option_def)
 
-lemma sup_Some [simp, code]:
-  "Some x \<squnion> Some y = Some (x \<squnion> y)"
+lemma sup_Some [simp, code]: "Some x \<squnion> Some y = Some (x \<squnion> y)"
   by (simp add: sup_option_def)
 
 instance ..
 
 end
 
-instantiation option :: (semilattice_inf) semilattice_inf
-begin
-
-instance proof
+instance option :: (semilattice_inf) semilattice_inf
+proof
   fix x y z :: "'a option"
   show "x \<sqinter> y \<le> x"
-    by - (cases x, simp_all, cases y, simp_all)
+    by (cases x, simp_all, cases y, simp_all)
   show "x \<sqinter> y \<le> y"
-    by - (cases x, simp_all, cases y, simp_all)
+    by (cases x, simp_all, cases y, simp_all)
   show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
-    by - (cases x, simp_all, cases y, simp_all, cases z, simp_all)
+    by (cases x, simp_all, cases y, simp_all, cases z, simp_all)
 qed
-  
-end
 
-instantiation option :: (semilattice_sup) semilattice_sup
-begin
-
-instance proof
+instance option :: (semilattice_sup) semilattice_sup
+proof
   fix x y z :: "'a option"
   show "x \<le> x \<squnion> y"
-    by - (cases x, simp_all, cases y, simp_all)
+    by (cases x, simp_all, cases y, simp_all)
   show "y \<le> x \<squnion> y"
-    by - (cases x, simp_all, cases y, simp_all)
+    by (cases x, simp_all, cases y, simp_all)
   fix x y z :: "'a option"
   show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x"
-    by - (cases y, simp_all, cases z, simp_all, cases x, simp_all)
+    by (cases y, simp_all, cases z, simp_all, cases x, simp_all)
 qed
 
-end
-
 instance option :: (lattice) lattice ..
 
 instance option :: (lattice) bounded_lattice_bot ..
@@ -210,8 +198,8 @@
 proof
   fix x y z :: "'a option"
   show "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
-    by - (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
-qed 
+    by (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
+qed
 
 instantiation option :: (complete_lattice) complete_lattice
 begin
@@ -219,22 +207,20 @@
 definition Inf_option :: "'a option set \<Rightarrow> 'a option" where
   "\<Sqinter>A = (if None \<in> A then None else Some (\<Sqinter>Option.these A))"
 
-lemma None_in_Inf [simp]:
-  "None \<in> A \<Longrightarrow> \<Sqinter>A = None"
+lemma None_in_Inf [simp]: "None \<in> A \<Longrightarrow> \<Sqinter>A = None"
   by (simp add: Inf_option_def)
 
 definition Sup_option :: "'a option set \<Rightarrow> 'a option" where
   "\<Squnion>A = (if A = {} \<or> A = {None} then None else Some (\<Squnion>Option.these A))"
 
-lemma empty_Sup [simp]:
-  "\<Squnion>{} = None"
+lemma empty_Sup [simp]: "\<Squnion>{} = None"
   by (simp add: Sup_option_def)
 
-lemma singleton_None_Sup [simp]:
-  "\<Squnion>{None} = None"
+lemma singleton_None_Sup [simp]: "\<Squnion>{None} = None"
   by (simp add: Sup_option_def)
 
-instance proof
+instance
+proof
   fix x :: "'a option" and A
   assume "x \<in> A"
   then show "\<Sqinter>A \<le> x"
@@ -274,10 +260,9 @@
   qed
 next
   show "\<Squnion>{} = (\<bottom>::'a option)"
-  by (auto simp: bot_option_def)
-next
+    by (auto simp: bot_option_def)
   show "\<Sqinter>{} = (\<top>::'a option)"
-  by (auto simp: top_option_def Inf_option_def)
+    by (auto simp: top_option_def Inf_option_def)
 qed
 
 end
@@ -298,10 +283,8 @@
   "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
   using Some_Sup [of "f ` A"] by (simp add: comp_def)
 
-instantiation option :: (complete_distrib_lattice) complete_distrib_lattice
-begin
-
-instance proof
+instance option :: (complete_distrib_lattice) complete_distrib_lattice
+proof
   fix a :: "'a option" and B
   show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
   proof (cases a)
@@ -354,14 +337,7 @@
   qed
 qed
 
-end
-
-instantiation option :: (complete_linorder) complete_linorder
-begin
-
-instance ..
-
-end
+instance option :: (complete_linorder) complete_linorder ..
 
 
 no_notation
@@ -379,4 +355,3 @@
   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
 
 end
-
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -392,13 +392,12 @@
 definition
   [code]: "HOL.equal (p::'a poly) q \<longleftrightarrow> HOL.equal (coeffs p) (coeffs q)"
 
-instance proof
-qed (simp add: equal equal_poly_def coeffs_eq_iff)
+instance
+  by standard (simp add: equal equal_poly_def coeffs_eq_iff)
 
 end
 
-lemma [code nbe]:
-  "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
+lemma [code nbe]: "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
   by (fact equal_refl)
 
 definition is_zero :: "'a::zero poly \<Rightarrow> bool"
@@ -510,15 +509,16 @@
 lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   is "\<lambda>p q n. coeff p n + coeff q n"
 proof -
-  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
+  fix q p :: "'a poly"
+  show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
     using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
 qed
 
-lemma coeff_add [simp]:
-  "coeff (p + q) n = coeff p n + coeff q n"
+lemma coeff_add [simp]: "coeff (p + q) n = coeff p n + coeff q n"
   by (simp add: plus_poly.rep_eq)
 
-instance proof
+instance
+proof
   fix p q r :: "'a poly"
   show "(p + q) + r = p + (q + r)"
     by (simp add: poly_eq_iff add.assoc)
@@ -536,15 +536,16 @@
 lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   is "\<lambda>p q n. coeff p n - coeff q n"
 proof -
-  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
+  fix q p :: "'a poly"
+  show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
     using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
 qed
 
-lemma coeff_diff [simp]:
-  "coeff (p - q) n = coeff p n - coeff q n"
+lemma coeff_diff [simp]: "coeff (p - q) n = coeff p n - coeff q n"
   by (simp add: minus_poly.rep_eq)
 
-instance proof
+instance
+proof
   fix p q r :: "'a poly"
   show "p + q - p = q"
     by (simp add: poly_eq_iff)
@@ -560,14 +561,16 @@
 lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
   is "\<lambda>p n. - coeff p n"
 proof -
-  fix p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
+  fix p :: "'a poly"
+  show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
     using MOST_coeff_eq_0 by simp
 qed
 
 lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
   by (simp add: uminus_poly.rep_eq)
 
-instance proof
+instance
+proof
   fix p q :: "'a poly"
   show "- p + p = 0"
     by (simp add: poly_eq_iff)
@@ -663,7 +666,8 @@
   { fix xs ys :: "'a list" and n
     have "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n"
     proof (induct xs ys arbitrary: n rule: plus_coeffs.induct)
-      case (3 x xs y ys n) then show ?case by (cases n) (auto simp add: cCons_def)
+      case (3 x xs y ys n)
+      then show ?case by (cases n) (auto simp add: cCons_def)
     qed simp_all }
   note * = this
   { fix xs ys :: "'a list"
@@ -825,7 +829,8 @@
   shows "(p + q) * r = p * r + q * r"
   by (induct r) (simp add: mult_poly_0, simp add: smult_distribs algebra_simps)
 
-instance proof
+instance
+proof
   fix p q r :: "'a poly"
   show 0: "0 * p = 0"
     by (rule mult_poly_0_left)
@@ -861,18 +866,17 @@
 done
 
 lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
-  by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc)
+  by (induct m) (simp add: monom_0 smult_monom, simp add: monom_Suc)
 
 instantiation poly :: (comm_semiring_1) comm_semiring_1
 begin
 
-definition one_poly_def:
-  "1 = pCons 1 0"
+definition one_poly_def: "1 = pCons 1 0"
 
-instance proof
-  fix p :: "'a poly" show "1 * p = p"
+instance
+proof
+  show "1 * p = p" for p :: "'a poly"
     unfolding one_poly_def by simp
-next
   show "0 \<noteq> (1::'a poly)"
     unfolding one_poly_def by simp
 qed
@@ -1063,8 +1067,9 @@
 definition
   "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
 
-instance proof
-  fix x y :: "'a poly"
+instance
+proof
+  fix x y z :: "'a poly"
   show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
     unfolding less_eq_poly_def less_poly_def
     apply safe
@@ -1072,50 +1077,34 @@
     apply (drule (1) pos_poly_add)
     apply simp
     done
-next
-  fix x :: "'a poly" show "x \<le> x"
+  show "x \<le> x"
     unfolding less_eq_poly_def by simp
-next
-  fix x y z :: "'a poly"
-  assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
+  show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
     unfolding less_eq_poly_def
     apply safe
     apply (drule (1) pos_poly_add)
     apply (simp add: algebra_simps)
     done
-next
-  fix x y :: "'a poly"
-  assume "x \<le> y" and "y \<le> x" thus "x = y"
+  show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
     unfolding less_eq_poly_def
     apply safe
     apply (drule (1) pos_poly_add)
     apply simp
     done
-next
-  fix x y z :: "'a poly"
-  assume "x \<le> y" thus "z + x \<le> z + y"
+  show "x \<le> y \<Longrightarrow> z + x \<le> z + y"
     unfolding less_eq_poly_def
     apply safe
     apply (simp add: algebra_simps)
     done
-next
-  fix x y :: "'a poly"
   show "x \<le> y \<or> y \<le> x"
     unfolding less_eq_poly_def
     using pos_poly_total [of "x - y"]
     by auto
-next
-  fix x y z :: "'a poly"
-  assume "x < y" and "0 < z"
-  thus "z * x < z * y"
+  show "x < y \<Longrightarrow> 0 < z \<Longrightarrow> z * x < z * y"
     unfolding less_poly_def
     by (simp add: right_diff_distrib [symmetric] pos_poly_mult)
-next
-  fix x :: "'a poly"
   show "\<bar>x\<bar> = (if x < 0 then - x else x)"
     by (rule abs_poly_def)
-next
-  fix x :: "'a poly"
   show "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
     by (rule sgn_poly_def)
 qed
@@ -1410,7 +1399,8 @@
     by (simp add: div_poly_eq mod_poly_eq)
 qed
 
-instance proof
+instance
+proof
   fix x y :: "'a poly"
   show "x div y * y + x mod y = x"
     using pdivmod_rel [of x y]
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Prefix_Order.thy
--- a/src/HOL/Library/Prefix_Order.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Prefix_Order.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -14,7 +14,8 @@
 definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys"
 definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
 
-instance by (default, unfold less_eq_list_def less_list_def) auto
+instance
+  by standard (auto simp: less_eq_list_def less_list_def)
 
 end
 
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Product_Lexorder.thy
--- a/src/HOL/Library/Product_Lexorder.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Product_Lexorder.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -37,13 +37,13 @@
   by (auto simp add: less_prod_def le_less)
 
 instance prod :: (preorder, preorder) preorder
-  by default (auto simp: less_eq_prod_def less_prod_def less_le_not_le intro: order_trans)
+  by standard (auto simp: less_eq_prod_def less_prod_def less_le_not_le intro: order_trans)
 
 instance prod :: (order, order) order
-  by default (auto simp add: less_eq_prod_def)
+  by standard (auto simp add: less_eq_prod_def)
 
 instance prod :: (linorder, linorder) linorder
-  by default (auto simp: less_eq_prod_def)
+  by standard (auto simp: less_eq_prod_def)
 
 instantiation prod :: (linorder, linorder) distrib_lattice
 begin
@@ -55,7 +55,7 @@
   "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
 
 instance
-  by default (auto simp add: inf_prod_def sup_prod_def max_min_distrib2)
+  by standard (auto simp add: inf_prod_def sup_prod_def max_min_distrib2)
 
 end
 
@@ -70,7 +70,7 @@
 end
 
 instance prod :: (order_bot, order_bot) order_bot
-  by default (auto simp add: bot_prod_def)
+  by standard (auto simp add: bot_prod_def)
 
 instantiation prod :: (top, top) top
 begin
@@ -83,7 +83,7 @@
 end
 
 instance prod :: (order_top, order_top) order_top
-  by default (auto simp add: top_prod_def)
+  by standard (auto simp add: top_prod_def)
 
 instance prod :: (wellorder, wellorder) wellorder
 proof
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Product_Order.thy
--- a/src/HOL/Library/Product_Order.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Product_Order.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -49,7 +49,7 @@
 qed
 
 instance prod :: (order, order) order
-  by default auto
+  by standard auto
 
 
 subsection \<open>Binary infimum and supremum\<close>
@@ -57,8 +57,7 @@
 instantiation prod :: (inf, inf) inf
 begin
 
-definition
-  "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
+definition "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
 
 lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
   unfolding inf_prod_def by simp
@@ -69,11 +68,12 @@
 lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
   unfolding inf_prod_def by simp
 
-instance proof qed
+instance ..
+
 end
 
 instance prod :: (semilattice_inf, semilattice_inf) semilattice_inf
-  by default auto
+  by standard auto
 
 
 instantiation prod :: (sup, sup) sup
@@ -91,16 +91,17 @@
 lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
   unfolding sup_prod_def by simp
 
-instance proof qed
+instance ..
+
 end
 
 instance prod :: (semilattice_sup, semilattice_sup) semilattice_sup
-  by default auto
+  by standard auto
 
 instance prod :: (lattice, lattice) lattice ..
 
 instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
-  by default (auto simp add: sup_inf_distrib1)
+  by standard (auto simp add: sup_inf_distrib1)
 
 
 subsection \<open>Top and bottom elements\<close>
@@ -125,7 +126,7 @@
   unfolding top_prod_def by simp
 
 instance prod :: (order_top, order_top) order_top
-  by default (auto simp add: top_prod_def)
+  by standard (auto simp add: top_prod_def)
 
 instantiation prod :: (bot, bot) bot
 begin
@@ -147,12 +148,12 @@
   unfolding bot_prod_def by simp
 
 instance prod :: (order_bot, order_bot) order_bot
-  by default (auto simp add: bot_prod_def)
+  by standard (auto simp add: bot_prod_def)
 
 instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
 
 instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
-  by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
+  by standard (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
 
 
 subsection \<open>Complete lattice operations\<close>
@@ -160,28 +161,28 @@
 instantiation prod :: (Inf, Inf) Inf
 begin
 
-definition
-  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
+definition "Inf A = (INF x:A. fst x, INF x:A. snd x)"
 
-instance proof qed
+instance ..
+
 end
 
 instantiation prod :: (Sup, Sup) Sup
 begin
 
-definition
-  "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
+definition "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
 
-instance proof qed
+instance ..
+
 end
 
 instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
     conditionally_complete_lattice
-  by default (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
+  by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
     INF_def SUP_def simp del: Inf_image_eq Sup_image_eq intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
 
 instance prod :: (complete_lattice, complete_lattice) complete_lattice
-  by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
+  by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
     INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
 
 lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
@@ -231,9 +232,8 @@
 
 (* Contribution: Alessandro Coglio *)
 
-instance prod ::
-  (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
-proof (default, goals)
+instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
+proof (standard, goals)
   case 1
   then show ?case
     by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Product_Vector.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -25,7 +25,8 @@
 lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)"
   unfolding scaleR_prod_def by simp
 
-instance proof
+instance
+proof
   fix a b :: real and x y :: "'a \<times> 'b"
   show "scaleR a (x + y) = scaleR a x + scaleR a y"
     by (simp add: prod_eq_iff scaleR_right_distrib)
@@ -58,7 +59,8 @@
   shows "open S"
 using assms unfolding open_prod_def by fast
 
-instance proof
+instance
+proof
   show "open (UNIV :: ('a \<times> 'b) set)"
     unfolding open_prod_def by auto
 next
@@ -277,7 +279,8 @@
 lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
   unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
 
-instance proof
+instance
+proof
   fix x y :: "'a \<times> 'b"
   show "dist x y = 0 \<longleftrightarrow> x = y"
     unfolding dist_prod_def prod_eq_iff by simp
@@ -406,7 +409,8 @@
 lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<^sup>2 + (norm b)\<^sup>2)"
   unfolding norm_prod_def by simp
 
-instance proof
+instance
+proof
   fix r :: real and x y :: "'a \<times> 'b"
   show "norm x = 0 \<longleftrightarrow> x = 0"
     unfolding norm_prod_def
@@ -510,7 +514,8 @@
 lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
   unfolding inner_prod_def by simp
 
-instance proof
+instance
+proof
   fix r :: real
   fix x y z :: "'a::real_inner \<times> 'b::real_inner"
   show "inner x y = inner y x"
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Product_plus.thy
--- a/src/HOL/Library/Product_plus.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Product_plus.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -81,41 +81,56 @@
 subsection \<open>Class instances\<close>
 
 instance prod :: (semigroup_add, semigroup_add) semigroup_add
-  by default (simp add: prod_eq_iff add.assoc)
+  by standard (simp add: prod_eq_iff add.assoc)
 
 instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
-  by default (simp add: prod_eq_iff add.commute)
+  by standard (simp add: prod_eq_iff add.commute)
 
 instance prod :: (monoid_add, monoid_add) monoid_add
-  by default (simp_all add: prod_eq_iff)
+  by standard (simp_all add: prod_eq_iff)
 
 instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
-  by default (simp add: prod_eq_iff)
+  by standard (simp add: prod_eq_iff)
 
-instance prod ::
-  (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
-    by default (simp_all add: prod_eq_iff)
+instance prod :: (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
+    by standard (simp_all add: prod_eq_iff)
 
-instance prod ::
-  (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
-    by default (simp_all add: prod_eq_iff diff_diff_eq)
+instance prod :: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
+    by standard (simp_all add: prod_eq_iff diff_diff_eq)
 
-instance prod ::
-  (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
+instance prod :: (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
 
 instance prod :: (group_add, group_add) group_add
-  by default (simp_all add: prod_eq_iff)
+  by standard (simp_all add: prod_eq_iff)
 
 instance prod :: (ab_group_add, ab_group_add) ab_group_add
-  by default (simp_all add: prod_eq_iff)
+  by standard (simp_all add: prod_eq_iff)
 
 lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
-by (cases "finite A", induct set: finite, simp_all)
+proof (cases "finite A")
+  case True
+  then show ?thesis by induct simp_all
+next
+  case False
+  then show ?thesis by simp
+qed
 
 lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
-by (cases "finite A", induct set: finite, simp_all)
+proof (cases "finite A")
+  case True
+  then show ?thesis by induct simp_all
+next
+  case False
+  then show ?thesis by simp
+qed
 
 lemma setsum_prod: "(\<Sum>x\<in>A. (f x, g x)) = (\<Sum>x\<in>A. f x, \<Sum>x\<in>A. g x)"
-by (cases "finite A", induct set: finite) (simp_all add: zero_prod_def)
+proof (cases "finite A")
+  case True
+  then show ?thesis by induct (simp_all add: zero_prod_def)
+next
+  case False
+  then show ?thesis by (simp add: zero_prod_def)
+qed
 
 end
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/RBT_Set.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -621,14 +621,17 @@
 lemma image_Set [code]:
   "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
 proof -
-  have "comp_fun_commute (\<lambda>k. Set.insert (f k))" by default auto
-  then show ?thesis by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
+  have "comp_fun_commute (\<lambda>k. Set.insert (f k))"
+    by standard auto
+  then show ?thesis
+    by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
 qed
 
 lemma Ball_Set [code]:
   "Ball (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
 proof -
-  have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
+  have "comp_fun_commute (\<lambda>k s. s \<and> P k)"
+    by standard auto
   then show ?thesis 
     by (simp add: foldi_fold_conj[symmetric] Ball_fold finite_fold_fold_keys)
 qed
@@ -636,7 +639,8 @@
 lemma Bex_Set [code]:
   "Bex (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
 proof -
-  have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
+  have "comp_fun_commute (\<lambda>k s. s \<or> P k)"
+    by standard auto
   then show ?thesis 
     by (simp add: foldi_fold_disj[symmetric] Bex_fold finite_fold_fold_keys)
 qed
@@ -670,7 +674,8 @@
 lemma setsum_Set [code]:
   "setsum f (Set xs) = fold_keys (plus o f) xs 0"
 proof -
-  have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: ac_simps)
+  have "comp_fun_commute (\<lambda>x. op + (f x))"
+    by standard (auto simp: ac_simps)
   then show ?thesis 
     by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
 qed
@@ -695,23 +700,23 @@
     by(auto split: rbt.split unit.split color.split)
 qed
 
-lemma Pow_Set [code]:
-  "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
-by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
+lemma Pow_Set [code]: "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
+  by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
 
 lemma product_Set [code]:
   "Product_Type.product (Set t1) (Set t2) = 
     fold_keys (\<lambda>x A. fold_keys (\<lambda>y. Set.insert (x, y)) t2 A) t1 {}"
 proof -
-  have *:"\<And>x. comp_fun_commute (\<lambda>y. Set.insert (x, y))" by default auto
+  have *: "comp_fun_commute (\<lambda>y. Set.insert (x, y))" for x
+    by standard auto
   show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_product_fold, of "Set t2" "{}" "t1"]  
     by (simp add: product_fold Product_Type.product_def finite_fold_fold_keys[OF *])
 qed
 
-lemma Id_on_Set [code]:
-  "Id_on (Set t) =  fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
+lemma Id_on_Set [code]: "Id_on (Set t) =  fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
 proof -
-  have "comp_fun_commute (\<lambda>x. Set.insert (x, x))" by default auto
+  have "comp_fun_commute (\<lambda>x. Set.insert (x, x))"
+    by standard auto
   then show ?thesis
     by (auto simp add: Id_on_fold intro!: finite_fold_fold_keys)
 qed
@@ -728,10 +733,12 @@
   "(Set t1) O (Set t2) = fold_keys 
     (\<lambda>(x,y) A. fold_keys (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') t2 A) t1 {}"
 proof -
-  interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
+  interpret comp_fun_idem Set.insert
+    by (fact comp_fun_idem_insert)
   have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')"
-    by default (auto simp add: fun_eq_iff)
-  show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
+    by standard (auto simp add: fun_eq_iff)
+  show ?thesis
+    using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
     by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
 qed
 
@@ -759,11 +766,13 @@
   fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   shows "Inf (Set t) = (if RBT.is_empty t then top else r_min_opt t)"
 proof -
-  have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
+  have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)"
+    by standard (simp add: fun_eq_iff ac_simps)
   then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
     by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
   then show ?thesis 
-    by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
+    by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric]
+      r_min_eq_r_min_opt[symmetric] r_min_alt_def)
 qed
 
 definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x"
@@ -775,7 +784,7 @@
   shows "INFIMUM (Set t) f = fold_keys (inf \<circ> f) t top"
 proof -
   have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
-    by default (auto simp add: fun_eq_iff ac_simps)
+    by standard (auto simp add: fun_eq_iff ac_simps)
   then show ?thesis
     by (auto simp: INF_fold_inf finite_fold_fold_keys)
 qed
@@ -800,14 +809,17 @@
   fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   shows "Sup (Set t) = (if RBT.is_empty t then bot else r_max_opt t)"
 proof -
-  have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
+  have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)"
+    by standard (simp add: fun_eq_iff ac_simps)
   then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
     by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
   then show ?thesis 
-    by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
+    by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric]
+      r_max_eq_r_max_opt[symmetric] r_max_alt_def)
 qed
 
-definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x"
+definition Sup' :: "'a :: {linorder,complete_lattice} set \<Rightarrow> 'a"
+  where [code del]: "Sup' x = Sup x"
 declare Sup'_def[symmetric, code_unfold]
 declare Sup_Set_fold[folded Sup'_def, code]
 
@@ -816,30 +828,34 @@
   shows "SUPREMUM (Set t) f = fold_keys (sup \<circ> f) t bot"
 proof -
   have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
-    by default (auto simp add: fun_eq_iff ac_simps)
+    by standard (auto simp add: fun_eq_iff ac_simps)
   then show ?thesis
     by (auto simp: SUP_fold_sup finite_fold_fold_keys)
 qed
 
-lemma sorted_list_set[code]:
-  "sorted_list_of_set (Set t) = RBT.keys t"
-by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
+lemma sorted_list_set[code]: "sorted_list_of_set (Set t) = RBT.keys t"
+  by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
 
 lemma Bleast_code [code]:
- "Bleast (Set t) P = (case filter P (RBT.keys t) of
-    x#xs \<Rightarrow> x |
-    [] \<Rightarrow> abort_Bleast (Set t) P)"
+  "Bleast (Set t) P =
+    (case filter P (RBT.keys t) of
+      x # xs \<Rightarrow> x
+    | [] \<Rightarrow> abort_Bleast (Set t) P)"
 proof (cases "filter P (RBT.keys t)")
-  case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
+  case Nil
+  thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
 next
   case (Cons x ys)
   have "(LEAST x. x \<in> Set t \<and> P x) = x"
   proof (rule Least_equality)
-    show "x \<in> Set t \<and> P x" using Cons[symmetric]
-      by(auto simp add: set_keys Cons_eq_filter_iff)
+    show "x \<in> Set t \<and> P x"
+      using Cons[symmetric]
+      by (auto simp add: set_keys Cons_eq_filter_iff)
     next
-      fix y assume "y : Set t \<and> P y"
-      then show "x \<le> y" using Cons[symmetric]
+      fix y
+      assume "y \<in> Set t \<and> P y"
+      then show "x \<le> y"
+        using Cons[symmetric]
         by(auto simp add: set_keys Cons_eq_filter_iff)
           (metis sorted_Cons sorted_append sorted_keys)
   qed
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Saturated.thy
--- a/src/HOL/Library/Saturated.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Saturated.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -61,7 +61,8 @@
   less_sat_def: "x < y \<longleftrightarrow> nat_of x < nat_of y"
 
 instance
-by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
+  by standard
+    (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
 
 end
 
@@ -106,8 +107,9 @@
   "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
   by (simp add: times_sat_def)
 
-instance proof
-  fix a b c :: "('a::len) sat"
+instance
+proof
+  fix a b c :: "'a::len sat"
   show "a * b * c = a * (b * c)"
   proof(cases "a = 0")
     case True thus ?thesis by (simp add: sat_eq_iff)
@@ -120,14 +122,10 @@
         by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult.assoc min.assoc min.absorb2)
     qed
   qed
-next
-  fix a :: "('a::len) sat"
   show "1 * a = a"
     apply (simp add: sat_eq_iff)
     apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min.absorb_iff1 min_nat_of_len_of nat_mult_1_right mult.commute)
     done
-next
-  fix a b c :: "('a::len) sat"
   show "(a + b) * c = a * c + b * c"
   proof(cases "c = 0")
     case True thus ?thesis by (simp add: sat_eq_iff)
@@ -143,7 +141,8 @@
 begin
 
 instance
-by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
+  by standard
+    (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
 
 end
 
@@ -183,43 +182,33 @@
 instantiation sat :: (len) equal
 begin
 
-definition
-  "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
+definition "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
 
-instance proof
-qed (simp add: equal_sat_def nat_of_inject)
+instance
+  by standard (simp add: equal_sat_def nat_of_inject)
 
 end
 
 instantiation sat :: (len) "{bounded_lattice, distrib_lattice}"
 begin
 
-definition
-  "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
-
-definition
-  "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
+definition "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
+definition "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
+definition "bot = (0 :: 'a sat)"
+definition "top = Sat (len_of TYPE('a))"
 
-definition
-  "bot = (0 :: 'a sat)"
-
-definition
-  "top = Sat (len_of TYPE('a))"
-
-instance proof
-qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def max_min_distrib2,
-  simp_all add: less_eq_sat_def)
+instance
+  by standard
+    (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def max_min_distrib2,
+      simp_all add: less_eq_sat_def)
 
 end
 
 instantiation sat :: (len) "{Inf, Sup}"
 begin
 
-definition
-  "Inf = (semilattice_neutr_set.F min top :: 'a sat set \<Rightarrow> 'a sat)"
-
-definition
-  "Sup = (semilattice_neutr_set.F max bot :: 'a sat set \<Rightarrow> 'a sat)"
+definition "Inf = (semilattice_neutr_set.F min top :: 'a sat set \<Rightarrow> 'a sat)"
+definition "Sup = (semilattice_neutr_set.F max bot :: 'a sat set \<Rightarrow> 'a sat)"
 
 instance ..
 
@@ -229,16 +218,20 @@
 where
   "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
 proof -
-  show "semilattice_neutr_set min (top :: 'a sat)" by default (simp add: min_def)
-  show "semilattice_neutr_set.F min (top :: 'a sat) = Inf" by (simp add: Inf_sat_def)
+  show "semilattice_neutr_set min (top :: 'a sat)"
+    by standard (simp add: min_def)
+  show "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
+    by (simp add: Inf_sat_def)
 qed
 
 interpretation Sup_sat!: semilattice_neutr_set max "bot :: 'a::len sat"
 where
   "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
 proof -
-  show "semilattice_neutr_set max (bot :: 'a sat)" by default (simp add: max_def bot.extremum_unique)
-  show "semilattice_neutr_set.F max (bot :: 'a sat) = Sup" by (simp add: Sup_sat_def)
+  show "semilattice_neutr_set max (bot :: 'a sat)"
+    by standard (simp add: max_def bot.extremum_unique)
+  show "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
+    by (simp add: Sup_sat_def)
 qed
 
 instance sat :: (len) complete_lattice
@@ -271,10 +264,8 @@
 next
   show "Inf {} = (top::'a sat)"
     by (auto simp: top_sat_def)
-next
   show "Sup {} = (bot::'a sat)"
     by (auto simp: bot_sat_def)
 qed
 
 end
-
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Set_Algebras.thy
--- a/src/HOL/Library/Set_Algebras.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Set_Algebras.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -64,28 +64,28 @@
   "x =o A \<equiv> x \<in> A"
 
 instance set :: (semigroup_add) semigroup_add
-  by default (force simp add: set_plus_def add.assoc)
+  by standard (force simp add: set_plus_def add.assoc)
 
 instance set :: (ab_semigroup_add) ab_semigroup_add
-  by default (force simp add: set_plus_def add.commute)
+  by standard (force simp add: set_plus_def add.commute)
 
 instance set :: (monoid_add) monoid_add
-  by default (simp_all add: set_plus_def)
+  by standard (simp_all add: set_plus_def)
 
 instance set :: (comm_monoid_add) comm_monoid_add
-  by default (simp_all add: set_plus_def)
+  by standard (simp_all add: set_plus_def)
 
 instance set :: (semigroup_mult) semigroup_mult
-  by default (force simp add: set_times_def mult.assoc)
+  by standard (force simp add: set_times_def mult.assoc)
 
 instance set :: (ab_semigroup_mult) ab_semigroup_mult
-  by default (force simp add: set_times_def mult.commute)
+  by standard (force simp add: set_times_def mult.commute)
 
 instance set :: (monoid_mult) monoid_mult
-  by default (simp_all add: set_times_def)
+  by standard (simp_all add: set_times_def)
 
 instance set :: (comm_monoid_mult) comm_monoid_mult
-  by default (simp_all add: set_times_def)
+  by standard (simp_all add: set_times_def)
 
 lemma set_plus_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a + b \<in> C + D"
   by (auto simp add: set_plus_def)
diff -r 17ba2df56dee -r ade12ef2773c src/HOL/Library/Sublist.thy
--- a/src/HOL/Library/Sublist.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Sublist.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -18,10 +18,10 @@
   where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
 
 interpretation prefix_order: order prefixeq prefix
-  by default (auto simp: prefixeq_def prefix_def)
+  by standard (auto simp: prefixeq_def prefix_def)
 
 interpretation prefix_bot: order_bot Nil prefixeq prefix
-  by default (simp add: prefixeq_def)
+  by standard (simp add: prefixeq_def)
 
 lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
   unfolding prefixeq_def by blast