src/HOL/Hilbert_Choice.thy
changeset 21020 9af9ceb16d58
parent 18389 8352b1d3b639
child 21243 afffe1f72143
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Oct 13 18:14:12 2006 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Oct 13 18:15:18 2006 +0200
     1.3 @@ -419,7 +419,7 @@
     1.4  lemma GreatestM_nat_le:
     1.5    "P x ==> \<forall>y. P y --> m y < b
     1.6      ==> (m x::nat) <= m (GreatestM m P)"
     1.7 -  apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec])
     1.8 +  apply (blast dest: GreatestM_nat_lemma [THEN conjunct2, THEN spec, of P])
     1.9    done
    1.10  
    1.11