--- a/src/HOL/GCD.thy Sun Feb 15 08:17:46 2015 +0100
+++ b/src/HOL/GCD.thy Sun Feb 15 17:01:22 2015 +0100
@@ -334,8 +334,7 @@
+ gcd_nat: semilattice_neutr_order "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat" 0 "op dvd" "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)"
apply default
apply (auto intro: dvd_antisym dvd_trans)[4]
-apply (metis dvd.dual_order.refl gcd_unique_nat)
-apply (auto intro: dvdI elim: dvdE)
+apply (metis dvd.dual_order.refl gcd_unique_nat)+
done
interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
--- a/src/HOL/Lattices.thy Sun Feb 15 08:17:46 2015 +0100
+++ b/src/HOL/Lattices.thy Sun Feb 15 17:01:22 2015 +0100
@@ -37,7 +37,7 @@
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<prec>" 50)
assumes order_iff: "a \<preceq> b \<longleftrightarrow> a = a * b"
- and semilattice_strict_iff_order: "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
+ and strict_order_iff: "a \<prec> b \<longleftrightarrow> a = a * b \<and> a \<noteq> b"
begin
lemma orderI:
@@ -53,7 +53,7 @@
proof
fix a b
show "a \<prec> b \<longleftrightarrow> a \<preceq> b \<and> a \<noteq> b"
- by (fact semilattice_strict_iff_order)
+ by (simp add: order_iff strict_order_iff)
next
fix a
show "a \<preceq> a"
--- a/src/HOL/Number_Theory/Gauss.thy Sun Feb 15 08:17:46 2015 +0100
+++ b/src/HOL/Number_Theory/Gauss.thy Sun Feb 15 17:01:22 2015 +0100
@@ -161,8 +161,7 @@
lemma nonzero_mod_p:
fixes x::int shows "\<lbrakk>0 < x; x < int p\<rbrakk> \<Longrightarrow> [x \<noteq> 0](mod p)"
-by (metis Nat_Transfer.transfer_nat_int_function_closures(9) cong_less_imp_eq_int
- inf.semilattice_strict_iff_order int_less_0_conv le_numeral_extra(3) zero_less_imp_eq_int)
+ by (simp add: cong_int_def)
lemma A_ncong_p: "x \<in> A \<Longrightarrow> [x \<noteq> 0](mod p)"
by (rule nonzero_mod_p) (auto simp add: A_def)