Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hilbert_Choice.thy
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
isabelle