--- a/src/HOL/Algebra/Divisibility.thy Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Algebra/Divisibility.thy Sun Sep 13 22:56:52 2015 +0200
@@ -25,14 +25,14 @@
and r_cancel:
"\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
shows "monoid_cancel G"
- by default fact+
+ by standard fact+
lemma (in monoid_cancel) is_monoid_cancel:
"monoid_cancel G"
..
sublocale group \<subseteq> monoid_cancel
- by default simp_all
+ by standard simp_all
locale comm_monoid_cancel = monoid_cancel + comm_monoid
@@ -3640,7 +3640,7 @@
done
sublocale factorial_monoid \<subseteq> primeness_condition_monoid
- by default (rule irreducible_is_prime)
+ by standard (rule irreducible_is_prime)
lemma (in factorial_monoid) primeness_condition:
@@ -3649,10 +3649,10 @@
lemma (in factorial_monoid) gcd_condition [simp]:
shows "gcd_condition_monoid G"
- by default (rule gcdof_exists)
+ by standard (rule gcdof_exists)
sublocale factorial_monoid \<subseteq> gcd_condition_monoid
- by default (rule gcdof_exists)
+ by standard (rule gcdof_exists)
lemma (in factorial_monoid) division_weak_lattice [simp]:
shows "weak_lattice (division_rel G)"