author paulson Fri, 16 Feb 2001 13:47:06 +0100 changeset 11154 042015819774 parent 11153 950ede59c05a child 11155 603df40ef1e9
for the change to LEAST
```--- a/doc-src/TutorialI/Rules/Basic.thy	Fri Feb 16 13:37:21 2001 +0100
+++ b/doc-src/TutorialI/Rules/Basic.thy	Fri Feb 16 13:47:06 2001 +0100
@@ -228,7 +228,7 @@

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)
+apply (simp add: Least_def LeastM_def)

txt{*omit maybe?
@{subgoals[display,indent=0,margin=65]}
@@ -266,7 +266,7 @@

(*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)
+apply (simp add: Least_def LeastM_def)
by (blast intro: some_equality order_antisym);

theorem axiom_of_choice: "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)"```