1.1 --- a/doc-src/TutorialI/Rules/Basic.thy	Fri Feb 16 13:37:21 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Rules/Basic.thy	Fri Feb 16 13:47:06 2001 +0100
     1.3 @@ -228,7 +228,7 @@
     1.4  
     1.5  theorem Least_equality:
     1.6       "\<lbrakk> P (k::nat);  \<forall>x. P x \<longrightarrow> k \<le> x \<rbrakk> \<Longrightarrow> (LEAST x. P(x)) = k"
     1.7 -apply (simp add: Least_def)
     1.8 +apply (simp add: Least_def LeastM_def)
     1.9   
    1.10  txt{*omit maybe?
    1.11  @{subgoals[display,indent=0,margin=65]}
    1.12 @@ -266,7 +266,7 @@
    1.13  
    1.14  (*both can be done by blast, which however hasn't been introduced yet*)
    1.15  lemma "[| P (k::nat);  \<forall>x. P x \<longrightarrow> k \<le> x |] ==> (LEAST x. P(x)) = k";
    1.16 -apply (simp add: Least_def)
    1.17 +apply (simp add: Least_def LeastM_def)
    1.18  by (blast intro: some_equality order_antisym);
    1.19  
    1.20  theorem axiom_of_choice: "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"