# HG changeset patch
# User wenzelm
# Date 1404481828 -7200
# Node ID a609065c9e15da37370aa056a7e3d009f4fc3de7
# Parent  f5dbec155914c590b4a7c6bde280fa1076f3554e
revived unchecked theory (see cebaf814ca6e);

diff -r f5dbec155914 -r a609065c9e15 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Jul 04 15:46:13 2014 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Jul 04 15:50:28 2014 +0200
@@ -1451,6 +1451,7 @@
   \end{description}
 *}
 
+
 chapter {* Proof tools *}
 
 section {* Adhoc tuples *}
diff -r f5dbec155914 -r a609065c9e15 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Jul 04 15:46:13 2014 +0200
+++ b/src/HOL/ROOT	Fri Jul 04 15:50:28 2014 +0200
@@ -521,6 +521,7 @@
     "~~/src/HOL/Library/Transitive_Closure_Table"
     Cartouche_Examples
   theories
+    Adhoc_Overloading_Examples
     Iff_Oracle
     Coercion_Examples
     Higher_Order_Logic
diff -r f5dbec155914 -r a609065c9e15 src/HOL/ex/Adhoc_Overloading_Examples.thy
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Fri Jul 04 15:46:13 2014 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Fri Jul 04 15:50:28 2014 +0200
@@ -127,7 +127,8 @@
   apply (rule perms_imp_bij [OF f])
   apply (rule MOST_mono [OF perms_imp_MOST_eq [OF f]])
   apply (erule subst, rule inv_f_f)
-  by (rule bij_is_inj [OF perms_imp_bij [OF f]])
+  apply (rule bij_is_inj [OF perms_imp_bij [OF f]])
+  done
 
 lemma bij_Rep_perm: "bij (Rep_perm p)"
   using Rep_perm [of p] unfolding perms_def by simp
@@ -207,7 +208,11 @@
   PERMUTE permute_perm
 
 interpretation perm_permute: permute permute_perm
-  by (default) (simp add: diff_minus minus_add add_assoc permute_perm_def)+
+  apply default
+  unfolding permute_perm_def
+  apply simp
+  apply (simp only: diff_conv_add_uminus minus_add add_assoc)
+  done
 
 text {*Permuting functions.*}
 locale fun_permute =