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/Import/HOL/HOL4Base.thy
changeset 23290 c358025ad8db
parent 17727 83d64a461507
child 30952 7ab2716dd93b 
--- a/src/HOL/Import/HOL/HOL4Base.thy	Thu Jun 07 04:33:15 2007 +0200
+++ b/src/HOL/Import/HOL/HOL4Base.thy	Thu Jun 07 11:25:05 2007 +0200
@@ -5528,7 +5528,7 @@
   by (import rich_list IS_EL_FOLDL_MAP)
 
 lemma FILTER_FILTER: "ALL (P::'a::type => bool) (Q::'a::type => bool) l::'a::type list.
-   filter P (filter Q l) = [x::'a::type:l. P x & Q x]"
+   filter P (filter Q l) = [x::'a::type<-l. P x & Q x]"
   by (import rich_list FILTER_FILTER)
 
 lemma FCOMM_FOLDR_FLAT: "ALL (g::'a::type => 'a::type => 'a::type)
isabelle