--- a/doc-src/TutorialI/Rules/Basic.thy Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy Thu Jul 26 16:43:02 2001 +0200
@@ -309,13 +309,13 @@
theorem Least_equality:
"\<lbrakk> P (k::nat); \<forall>x. P x \<longrightarrow> k \<le> x \<rbrakk> \<Longrightarrow> (LEAST x. P(x)) = k"
-apply (simp add: Least_def LeastM_def)
+apply (simp add: Least_def)
txt{*omit maybe?
@{subgoals[display,indent=0,margin=65]}
*};
-apply (rule some_equality)
+apply (rule the_equality)
txt{*
@{subgoals[display,indent=0,margin=65]}