# HG changeset patch
# User nipkow
# Date 1495963935 -7200
# Node ID 440fe0937b92a4884c79562291dfb3f5d6732893
# Parent  dec96cb3fbe0c185dec69316fffd71ea973248dd
added is_arg_min

diff -r dec96cb3fbe0 -r 440fe0937b92 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Sun May 28 08:07:40 2017 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Sun May 28 11:32:15 2017 +0200
@@ -418,6 +418,7 @@
 @{const Lattices_Big.Min} & @{typeof Lattices_Big.Min}\\
 @{const Lattices_Big.Max} & @{typeof Lattices_Big.Max}\\
 @{const Lattices_Big.arg_min} & @{typeof Lattices_Big.arg_min}\\
+@{const Lattices_Big.is_arg_min} & @{typeof Lattices_Big.is_arg_min}\\
 \end{supertabular}
 
 \subsubsection*{Syntax}
diff -r dec96cb3fbe0 -r 440fe0937b92 src/Doc/Tutorial/Rules/Basic.thy
--- a/src/Doc/Tutorial/Rules/Basic.thy	Sun May 28 08:07:40 2017 +0200
+++ b/src/Doc/Tutorial/Rules/Basic.thy	Sun May 28 11:32:15 2017 +0200
@@ -378,8 +378,8 @@
 
 (*both can be done by blast, which however hasn't been introduced yet*)
 lemma "[| P (k::nat);  \<forall>x. P x \<longrightarrow> k \<le> x |] ==> (LEAST x. P(x)) = k"
-apply (simp add: Least_def LeastM_def)
-by (blast intro: some_equality order_antisym)
+apply (simp add: Least_def)
+by (blast intro: order_antisym)
 
 theorem axiom_of_choice': "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"
 apply (rule exI [of _  "\<lambda>x. SOME y. P x y"])