1.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Jul 04 15:46:13 2014 +0200
     1.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Jul 04 15:50:28 2014 +0200
     1.3 @@ -1451,6 +1451,7 @@
     1.4    \end{description}
     1.5  *}
     1.6  
     1.7 +
     1.8  chapter {* Proof tools *}
     1.9  
    1.10  section {* Adhoc tuples *}

     2.1 --- a/src/HOL/ROOT	Fri Jul 04 15:46:13 2014 +0200
     2.2 +++ b/src/HOL/ROOT	Fri Jul 04 15:50:28 2014 +0200
     2.3 @@ -521,6 +521,7 @@
     2.4      "~~/src/HOL/Library/Transitive_Closure_Table"
     2.5      Cartouche_Examples
     2.6    theories
     2.7 +    Adhoc_Overloading_Examples
     2.8      Iff_Oracle
     2.9      Coercion_Examples
    2.10      Higher_Order_Logic

     3.1 --- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Fri Jul 04 15:46:13 2014 +0200
     3.2 +++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Fri Jul 04 15:50:28 2014 +0200
     3.3 @@ -127,7 +127,8 @@
     3.4    apply (rule perms_imp_bij [OF f])
     3.5    apply (rule MOST_mono [OF perms_imp_MOST_eq [OF f]])
     3.6    apply (erule subst, rule inv_f_f)
     3.7 -  by (rule bij_is_inj [OF perms_imp_bij [OF f]])
     3.8 +  apply (rule bij_is_inj [OF perms_imp_bij [OF f]])
     3.9 +  done
    3.10  
    3.11  lemma bij_Rep_perm: "bij (Rep_perm p)"
    3.12    using Rep_perm [of p] unfolding perms_def by simp
    3.13 @@ -207,7 +208,11 @@
    3.14    PERMUTE permute_perm
    3.15  
    3.16  interpretation perm_permute: permute permute_perm
    3.17 -  by (default) (simp add: diff_minus minus_add add_assoc permute_perm_def)+
    3.18 +  apply default
    3.19 +  unfolding permute_perm_def
    3.20 +  apply simp
    3.21 +  apply (simp only: diff_conv_add_uminus minus_add add_assoc)
    3.22 +  done
    3.23  
    3.24  text {*Permuting functions.*}
    3.25  locale fun_permute =