--- 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}
--- 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"])