src/HOL/Hilbert_Choice.thy
changeset 39950 f3c4849868b8
parent 39943 0ef551d47783
child 40702 cf26dd7395e4
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Tue Oct 05 10:30:50 2010 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Oct 05 10:59:12 2010 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4  
     1.5  subsection{*Axiom of Choice, Proved Using the Description Operator*}
     1.6  
     1.7 -lemma choice [meson_choice]: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
     1.8 +lemma choice: "\<forall>x. \<exists>y. Q x y ==> \<exists>f. \<forall>x. Q x (f x)"
     1.9  by (fast elim: someI)
    1.10  
    1.11  lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)"