# HG changeset patch
# User nipkow
# Date 1181208305 -7200
# Node ID c358025ad8db894d4f95568d00d72dca1748be46
# Parent  0cf371d943b15caf3850c5446f6f5a02c6b7ceba
filter syntax change

diff -r 0cf371d943b1 -r c358025ad8db src/HOL/Import/HOL/HOL4Base.thy
--- 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)
diff -r 0cf371d943b1 -r c358025ad8db src/HOL/Import/HOL/HOL4Prob.thy
--- a/src/HOL/Import/HOL/HOL4Prob.thy	Thu Jun 07 04:33:15 2007 +0200
+++ b/src/HOL/Import/HOL/HOL4Prob.thy	Thu Jun 07 11:25:05 2007 +0200
@@ -291,10 +291,10 @@
 lemma MEM_NIL_MAP_CONS: "ALL (x::'a::type) l::'a::type list list. ~ [] mem map (op # x) l"
   by (import prob_extra MEM_NIL_MAP_CONS)
 
-lemma FILTER_TRUE: "ALL l::'a::type list. [x::'a::type:l. True] = l"
+lemma FILTER_TRUE: "ALL l::'a::type list. [x::'a::type<-l. True] = l"
   by (import prob_extra FILTER_TRUE)
 
-lemma FILTER_FALSE: "ALL l::'a::type list. [x::'a::type:l. False] = []"
+lemma FILTER_FALSE: "ALL l::'a::type list. [x::'a::type<-l. False] = []"
   by (import prob_extra FILTER_FALSE)
 
 lemma FILTER_MEM: "ALL (P::'a::type => bool) (x::'a::type) l::'a::type list.
@@ -305,7 +305,7 @@
    x mem filter P l --> x mem l"
   by (import prob_extra MEM_FILTER)
 
-lemma FILTER_OUT_ELT: "ALL (x::'a::type) l::'a::type list. x mem l | [y::'a::type:l. y ~= x] = l"
+lemma FILTER_OUT_ELT: "ALL (x::'a::type) l::'a::type list. x mem l | [y::'a::type<-l. y ~= x] = l"
   by (import prob_extra FILTER_OUT_ELT)
 
 lemma IS_PREFIX_NIL: "ALL x::'a::type list. IS_PREFIX x [] & IS_PREFIX [] x = (x = [])"
@@ -1769,8 +1769,8 @@
 
 lemma MAP_CONS_TL_FILTER: "ALL (l::bool list list) b::bool.
    ~ [] mem l -->
-   map (op # b) (map tl [x::bool list:l. hd x = b]) =
-   [x::bool list:l. hd x = b]"
+   map (op # b) (map tl [x::bool list<-l. hd x = b]) =
+   [x::bool list<-l. hd x = b]"
   by (import prob_indep MAP_CONS_TL_FILTER)
 
 lemma ALG_COVER_SET_CASES_THM: "ALL l::bool list list.