src/HOL/Lattices_Big.thy

--- a/src/HOL/Lattices_Big.thy	Mon May 29 22:49:52 2017 +0200
+++ b/src/HOL/Lattices_Big.thy	Tue May 30 10:03:35 2017 +0200
@@ -985,7 +985,7 @@
   for f :: "'a \<Rightarrow> nat"
 by (blast dest: arg_max_nat_lemma [THEN conjunct2, THEN spec, of P])
 
-
+(*
 text \<open>\<^medskip> Specialization to \<open>GREATEST\<close>.\<close>
 
 (* LEAST ? *)
@@ -1012,5 +1012,5 @@
 apply (erule exE)
 apply (erule (1) GreatestI)
 done
-
+*)
 end