--- 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)
--- 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.