src/HOL/Algebra/Lattice.thy

--- a/src/HOL/Algebra/Lattice.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -921,7 +921,7 @@
 lemma (in weak_partial_order) weak_total_orderI:
   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   shows "weak_total_order L"
-  by default (rule total)
+  by standard (rule total)
 
 text {* Total orders are lattices. *}
 
@@ -985,7 +985,7 @@
     and inf_exists:
     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   shows "weak_complete_lattice L"
-  by default (auto intro: sup_exists inf_exists)
+  by standard (auto intro: sup_exists inf_exists)
 
 definition
   top :: "_ => 'a" ("\<top>\<index>")
@@ -1133,14 +1133,14 @@
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
 
 sublocale upper_semilattice < weak: weak_upper_semilattice
-  by default (rule sup_of_two_exists)
+  by standard (rule sup_of_two_exists)
 
 locale lower_semilattice = partial_order +
   assumes inf_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
 
 sublocale lower_semilattice < weak: weak_lower_semilattice
-  by default (rule inf_of_two_exists)
+  by standard (rule inf_of_two_exists)
 
 locale lattice = upper_semilattice + lower_semilattice
 
@@ -1191,19 +1191,19 @@
   assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
 
 sublocale total_order < weak: weak_total_order
-  by default (rule total_order_total)
+  by standard (rule total_order_total)
 
 text {* Introduction rule: the usual definition of total order *}
 
 lemma (in partial_order) total_orderI:
   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   shows "total_order L"
-  by default (rule total)
+  by standard (rule total)
 
 text {* Total orders are lattices. *}
 
 sublocale total_order < weak: lattice
-  by default (auto intro: sup_of_two_exists inf_of_two_exists)
+  by standard (auto intro: sup_of_two_exists inf_of_two_exists)
 
 
 text {* Complete lattices *}
@@ -1215,7 +1215,7 @@
     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
 
 sublocale complete_lattice < weak: weak_complete_lattice
-  by default (auto intro: sup_exists inf_exists)
+  by standard (auto intro: sup_exists inf_exists)
 
 text {* Introduction rule: the usual definition of complete lattice *}
 
@@ -1225,7 +1225,7 @@
     and inf_exists:
     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   shows "complete_lattice L"
-  by default (auto intro: sup_exists inf_exists)
+  by standard (auto intro: sup_exists inf_exists)
 
 theorem (in partial_order) complete_lattice_criterion1:
   assumes top_exists: "EX g. greatest L g (carrier L)"
@@ -1282,7 +1282,7 @@
   (is "complete_lattice ?L")
 proof (rule partial_order.complete_latticeI)
   show "partial_order ?L"
-    by default auto
+    by standard auto
 next
   fix B
   assume "B \<subseteq> carrier ?L"