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